Embedded Flight Software Verification (ESOVER)

Embedded Software Verifizierung

Embedded Flug-Software Verifizierung (ESOVER)

Zusammen mit dem Lab for Automated Reasoning (LARA) an der EPFL führt Ateleris eine Studie durch, die formale Softwareverifikation nutzt, um mathematisch bewiesen fehlerfreie Embedded Software zu entwickeln. Die Studie wird im Rahmen der Measure de Positionnement 2020 (MdP) des Swiss Space Office, Space Innovation und der ESA durchgeführt.

Ein bekanntes Sprichwort in der Softwareentwicklung lautet: “Softwaretests beweisen die Existenz von Fehlern, nicht deren Abwesenheit.” Diese Studie zielt darauf ab, eine kosteneffiziente formale Softwareverifikation in den Entwicklungsprozess von Raumfahrtanwendungen einzuführen, für die Entwicklung von nachweislich fehlerfreier Software.

Die formale Softwareverifikation ist eine Methode, die mathematische Beweise einsetzt, um sicherzustellen, dass sich Software entsprechend der gegebenen Spezifikation verhält, unabhängig der gewählten Eingabeparametern. Diese Korrektheit kann selbst dann nachgewiesen werden, wenn der Parameter-Raum so gross ist, dass das Testen aller Möglichkeiten nicht praktikabel wäre.

Die Studie basiert auf der von der LARA-Gruppe geleisteten Vorarbeit und verwendet die von der Gruppe entwickelte Stainless Plattform. Stainless ist ein Scala-basiertes formales Software-Verifikationstool. Im Rahmen dieses Projektes erweitert die Forschungsgruppe das Stainless-Framework, sodass ein grösserer und komplexerer Satz von Scala-Anweisungen verwendet werden können, sodass die Entwicklung sinnvoller Flugsoftwaremodulen möglich wird.

Als Proof of Concept wird Ateleris, mit ihrer Erfahrung im Programmieren der STIX-Flugsoftware, die Eignung dieses Ansatzes am STIX-Dateisystem testen. Zu diesem Zweck wird Ateleris das Dateisystem in Scala neu programmieren und dann mit Stainless verifizieren. So entsteht ein mathematisch nachgewiesenes, fehlerfreies Dateisystemmodul.

Um den Reintegrationsprozess des verifizierten Dateisystemmoduls in die originale STIX-Flugsoftware zu erleichtern, wird die Stainless-Plattform ausserdem mit einem neuen C-Code-Transpiler erweitert. Damit kann der verifizierte Scala-Code wieder in lauffähigen C-Code umgewandelt und reintegriert werden.

Weshalb setzen wir formale Software-Verifikation und Stainless ein?

Um korrekte Software zu erzeugen. Bei der formalen Verifikation wird bewiesen, dass die Software der Spezifikation entspricht, d. h. alle möglichen Eingabeparameter berücksichtigt wurden, sodass die Software auf alle möglichen Eingabeparameter korrekt reagieren wird.

Die Einhaltung von Anforderungen und Spezifikationen. Bei der formalen Verifikation werden die Anforderungen zu einem Teil der Software. Änderungen im Programmfluss werden automatisch erkannt und gemeldet, wenn dies die Spezifikation verletzt.

Erhöhte Effizienz bei der Softwareherstellung. Die Entwicklung von Flugsoftware wird in vielen Fällen in den Programmiersprachen C oder C++ durchgeführt. Die Programmierung in diesen Low-Level-Sprachen ist fehleranfällig und zeitaufwändig. Sie lassen undefiniertes Verhalten zu, bieten keine vollständige Typsicherheit und nur beschränktes Refactoring. Diese Einschränkungen führen nicht nur zu potenziell kritischen Fehlern (Pufferüberläufe, illegale Speicherzugriffe, Endlosschleifen und andere), sondern verlangsamen auch die Entwicklung. Für die Stainless-Plattform wird stattdessen die Programmiersprache Scala verwendet. Diese höherwertige Programmiersprache erhöht die Produktivität der Entwickler, da sie bessere Abstraktionen, Werkzeuge und Schutzmechanismen bietet.

Verbesserung der Software-Integration. Mit formal verifizierten Softwaremodulen werden die API und die Funktionalität der Softwarekomponenten verifiziert und als korrekt nachgewiesen – automatisch, nach jeder Änderung.

Zur Erzeugung von Code für mehrere Zielsysteme. Stainless kann Scala-Code automatisch zurück in C-Code übersetzen, was eine einfache Integration in die bestehende Codebasis ermöglicht. Diese Erweiterung hilft auch bei der Zertifizierung der Software, da die Raumfahrtindustrie gegenüber neuen Programmiersprachen oft skeptisch gegenüber steht. Indem wir Scala-Code automatisch nach C übersetzen und C-Code zur Qualifizierung einreichen, umgehen wir diese Bedenken.

Um wiederverwendbare verifizierte Module zu erhalten. Sobald ein Modul verifiziert wurde, kann es in anderen Einsatzgebieten wiederverwendet werden und ist immer noch korrekt. Diese Vielseitigkeit ermöglicht den Aufbau von Bibliotheken mit verifizierten Modulen, die in anderer Flugsoftware oder eingebetteten Systemen wiederverwendet werden können. Zum Beispiel sind verifizierte Datenstrukturen und Dateisysteme Module, die in einer Vielzahl von Anwendungen wiederverwendet werden können.

Zur Integration im Softwareentwicklungsprozess. Der vorgeschlagene Ansatz kann in den traditionellen Softwareentwicklungsprozess integriert werden und ergänzt andere Prozesse wie statische Verifikation und Unit- und Integrationstests (CI/CD).

Schlüsseltechnologien / -begriffe

  • Formale Software-Verifizierung
  • Scala Programmiersprache
  • C-Code Transpiler
  • Embedded Software-Entwicklung
  • Stainless Plattform
EPFL Logo

LARA ist eine Forschungsgruppe an der EPFL, die von Viktor Kunčak geleitet wird. Sie entwickeln präzise automatisierte Reasoning-Techniken: Tools, Algorithmen und Sprachen - das Ziel dieser Techniken ist es, die Entwicklung von verifizierten Computersystemen zu unterstützen.

Filip Schramka

Filip Schramka

Haben Sie Fragen? Senden Sie mir eine Nachricht!

Kontakt
Share on facebook
Share on twitter
Share on linkedin
Share on whatsapp
Share on email