Embedded Flight Software Verifizierung (ESOVER)

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).