Dieses Video demonstriert die Implementierung von speichersicherem Ada/SPARK-Code auf einem ST-Micro-Entwicklungsboard mit einem ARM Cortex-M55 Mikrocontroller und einer Neural Processing Unit (NPU) für Edge-KI-Anwendungen. Es zeigt, wie typische C-basierte Implementierungsfehler bei der Objekterkennung (wie Array-Grenzenüberschreitungen und ungültige Adresssuchen) zu undefiniertem Verhalten oder Systemabstürzen führen. Durch die Portierung der MCU-Logik nach Ada/SPARK und den Einsatz des GNAT-proof-Werkzeugs wird die Abwesenheit von Laufzeitfehlern mathematisch bewiesen, wodurch die Anwendung selbst bei fehlerhafter Dateneinspeisung absturzsicher bleibt.
Wichtigste Punkte & Zeitstempel
0:24 ARM Cortex-M55 & NPU: Ein ST-Micro-Entwicklungsboard mit integriertem ARM Cortex-M55 Mikrocontroller und einer Neural Processing Unit für Edge-KI-Fähigkeiten wird vorgestellt.
0:35 Objekterkennungs-Demo: Der Live-Stream einer Kamera wird von der NPU verarbeitet (liefert Bounding Boxes und Labels), während der MCU die Streams überlagert und auf dem Display ausgibt.
0:55 SPARK-Garantien: Verwendung von SPARK zur Gewährleistung der Abwesenheit von Laufzeitfehlern durch strikte Überprüfung von Variablen und Arrays innerhalb definierter Typgrenzen.
1:11 Fehler-Identifikation: Die statische Analyse deckte sechs potenzielle Programmierfehler auf, die zu undefiniertem Verhalten führen; ein physischer Button wird zur absichtlichen Fehler-Injektion genutzt.
1:42 Verhalten im Originalcode: Das Drücken des Buttons führt bei fehlerhaften Daten zu unvorhersehbarem Verhalten (Bounding Box klebt am linken Rand) oder zu einem vollständigen Systemabsturz durch ungültige Adresszugriffe.
2:18 Code-Portierung via LLM: Der ursprüngliche C-Code wurde während eines Fluges mithilfe eines Large Language Models nach Ada/SPARK übersetzt und mit dem GNAT proof-Werkzeug verifiziert und korrigiert.
2:50 Stabilität durch formale Verifizierung: Nach der Code-Migration führt die Injektion fehlerhafter Daten dank erzwungener Bereichsprüfungen nicht mehr zum Absturz der Anwendung.
Glossar
ARM Cortex-M55: Ein energieeffizienter 32-Bit-Mikrocontroller-Prozessorkern von ARM, der speziell für eingebettete Systeme und maschinelles Lernen optimiert ist.
NPU (Neural Processing Unit): Ein spezialisierter Prozessor, der hardwareseitig für die Beschleunigung von künstlicher Intelligenz und neuronalen Netzwerken optimiert ist.
MCU (Microcontroller Unit): Ein kompakter integrierter Schaltkreis, der einen Prozessorkern, Speicher und programmierbare Ein-/Ausgänge zur Steuerung elektronischer Geräte vereint.
SPARK: Eine streng typisierte Programmiersprache und ein formales Verifizierungswerkzeug, das auf Ada basiert und den mathematischen Nachweis der Abwesenheit von Laufzeitfehlern ermöglicht.
Ada: Eine hochentwickelte, stark typisierte Programmiersprache, die für kritische Echtzeitsysteme mit höchsten Anforderungen an Zuverlässigkeit und Sicherheit entwickelt wurde.
GNAT proof: Ein formales Verifizierungswerkzeug für SPARK- und Ada-Code, das den Quellcode statisch analysiert, um mathematisch zu beweisen, dass keine Laufzeitfehler auftreten.
LLM (Large Language Model): Ein auf künstlicher Intelligenz basierendes Sprachmodell, das in der Lage ist, Text zu generieren oder Quellcode automatisiert in andere Programmiersprachen zu übersetzen.
Edge-KI (Edge Artificial Intelligence): Die lokale Ausführung von KI-Algorithmen und neuronalen Netzen direkt auf Hardware-Geräten (wie Mikrocontrollern) anstelle einer Cloud-Infrastruktur.
Bounding Box: Ein in der Bildverarbeitung genutzter rechteckiger Rahmen, der die exakte Position und Ausdehnung eines erkannten Objekts in einem visuellen Stream markiert.