- Astrée
- Screenshots
- Beispiele
Astrée ist eine Software zur statischen Programmanalyse, die C-Programme automatisch auf Laufzeitfehler überprüft.
Astrée analysiert handgeschriebene oder automatisch erzeugte C-Programme mit komplexer Speichernutzung, aber ohne Rekursion oder dynamische Speicherallokation. Damit bietet sich Astrée vor allem zur Analyse von sicherheitskritischen eingebetteten Anwendungen an, insbesondere in den Bereichen Transport, Medizintechnik, Nuklearanlagen, Luft- und Raumfahrt.
Welche Laufzeiteigenschaften überprüft Astrée?
Astrée meldet folgende Arten von Laufzeitfehlern:
- Jeden Gebrauch der C-Sprache, der laut ISO/IEC 9899:1999, der internationalen Norm für C, ein undefiniertes Verhalten aufweist, z. B. Division durch null und Feldzugriffe außerhalb der gültigen Feldgrenzen.
- Jeden Gebrauch der C-Sprache, der gegen hardwarespezifische Einschränkungen der Implementierung verstößt, z. B. gegen Größenbeschränkungen für ganze Zahlen oder Grenzen für arithmetische Überläufe.
- Jeden Gebrauch der C-Sprache, der gegen benutzerspezifische Zusatzregeln verstößt, z. B. gegen einen Verbot der Anwendung von Modulararithmetik auf ganze Zahlen (auch wenn die Hardware diese ausdrücklich unterstützen mag).
- Jeden Verstoß gegen optionale benutzerdefinierte Annahmen zur Überprüfung
von sonstigen Laufzeiteigenschaften (ähnlich der „
assert“-Diagnostik).
Astrée kann an benutzerspezifische Anforderungen angepaßt und in bestehende Entwicklungsprozesse integriert werden.
Erfolgsgeschichten
Luftfahrt
© 2007 Xavier Rival2003 verifizierte Astrée die Abwesenheit von Laufzeitfehlern in der primären Flugkontrollsoftware des Fly-by-Wire-Systems eines Airbus-Modells. Die Analyse der 132.000 Zeilen C-Code erfolgte vollautomatisch und benötigte nur 80 Minuten auf einem 2,8-GHz-PC mit 300 MB Speicher (sowie nur 50 Minuten auf einem AMD-Athlon-64-Rechner mit 580 MB Speicher). 2004 wurde Astrée erweitert, um die Flugkontrollsoftware eines anderen Airbus-Modells zu analysieren.
Raumfahrt
Courtesy of NASAAnfang 2008 verifizierte Astrée die Abwesenheit von Laufzeitfehlern in der C-Version der Andocksoftware des Weltraumfrachters „Jules Verne“, des ersten automatischen Transferfahrzeugs der ESA. Die Analyse erfolgte vollautomatisch. Am 3. April 2008 dockte der Frachter erfolgreich an der Internationalen Raumstation (ISS) an.