Astrée ist eine Software zur statischen Programmanalyse, die C-Programme automatisch auf Laufzeitfehler überprüft.

Astrée-Screenshot
Astrée-Screenshot

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, insbe­sondere in den Bereichen Transport, Medizintechnik, Nuklearanlagen, Luft- und Raumfahrt.

Welche Laufzeiteigenschaften überprüft Astrée?

Astrée meldet folgende Arten von Laufzeitfehlern:

Astrée behandelt Gleitkommaberechnungen präzise und sicher und berücksichtigt alle möglichen Rundungsfehler.

Desweiteren meldet Astrée garantiert unerreichbaren Code und Lese­zugriffe auf un­initiali­sierte Variablen.

Astrée kann an benutzerspezifische Anforderungen angepaßt und in bestehende Entwick­lungs­prozesse integriert werden.

Erfolgsgeschichten

  • Luftfahrt

    Airbus A380© 2007 Xavier Rival

    2003 verifizierte Astrée die Abwesenheit von Laufzeitfehlern in der pri­mären Flug­kon­troll­software des Fly-by-Wire-Systems eines Airbus-Modells. Die Analyse der 132 000 Zei­len C-Code erfolgte vollautomatisch und be­nötigte nur 80 Minuten auf einem 2,8-GHz-PC mit 300 MB Speicher (sowie nur 50 Minu­ten 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

    Jules Verne ATVCourtesy of NASA

    Anfang 2008 verifizierte Astrée die Ab­we­senheit von Laufzeitfehlern in der C-Version der Andocksoftware des Welt­raumfrachters „Jules Verne“, des ersten automati­schen Transferfahrzeugs der ESA. Die Ana­lyse er­folgte vollautomatisch. Am 3. April 2008 dockte der Frachter erfolgreich an der Inter­nationalen Raumstation (ISS) an.


Ihre Vorteile

Astrée-Analysen sind…

  • sicher

    Manche Analysatoren berücksichtigen nicht alle möglichen Laufzeit­fehler, oder konzentrieren sich bewußt auf die wahrscheinlichsten davon. Solche Tools können daher nur zum statischen Testen benutzt werden (d. h. zum Auffinden von häufig auftretenden Bugs), nicht aber zur Verifikation (also zum Nachweis der Abwesenheit jeglicher Lauf­zeitfehler).

    Astrée-Analysen sind hingegen sicher. Das Tool berücksichtigt stets alle möglichen Laufzeitfehler, und wird niemals einen davon ver­schwei­gen. Dies ist unentbehrlich zur Verifikation von sicherheits­kritischer Software. Zugleich ist Astrée in der Lage, nur wenige oder gar keine Falschalarme zu produzieren.

  • automatisch

    Für manche Analysatoren (z. B. solche, die sich auf Computerbeweise verlassen) müssen Programme mit vielen Induktionsinvarianten anno­tiert werden.

    Astrée verlangt in aller Regel nur sehr wenige Annotationen. Bestimmte Arten von Programmen kann es sogar vollautomatisch untersuchen, ohne jede Hilfestellung vom Benutzer.

  • schnell

    Manche statischen Analysatoren benötigen sehr viel Zeit (typischer­weise mehrere Stunden zum Analysieren von 10 000 Codezeilen) oder verbrauchen extrem viel Speicher.

    Im Gegensatz dazu ist Astrée äußerst effizient und kann große in­dustrielle Anwendungen problemlos bewältigen. Beispielsweise benö­tigte Astrée nur 80 Minuten (auf einem 2,8-GHz-PC) zur Analyse der Flugsteuerungssoftware eines Airbus-Models, die aus 132 000 Zeilen C-Code besteht. Seit 2005 kann Astrée auf Multicore-Hardware laufen, was die Analysen noch weiter beschleunigt.

  • anpassungsfähig

    Universelle statische Analysatoren unterstützen alle in der jeweiligen Programmiersprache geschriebenen Anwendungen. Sie können nur in dieser Programmiersprache ausdrückbare Programmeigenschaften be­rücksichtigen. Domainspezifische statische Analysatoren schränken die Anwendungsklasse ein, um spezifische Programmstrukturen aus­nutzen zu können.

    Astrée hingegen ist spezialisierbar und kann an die Anwendungsklasse angepaßt werden. Dadurch können Eigenschaften der Anwendungs­klasse berücksichtigt werden, die zur Durchführung komplexer Beweise unerlässlich sind. Beispielsweise berücksichtigt Astrée bei Control/Command-Programmen die logischen und funktionalen Eigen­schaften der Control-and-Command-Theorie.

  • parametrisierbar

    Bei der statischer Programmanalyse gilt es stets, zwischen Analyse­präzision und Rechenaufwand abzuwägen. Sehr präzise Analysatoren sind in der Regel auch sehr langsam, während sehr schnelle Analy­satoren in der Regel sehr ungenau sind.

    Astrée hingegen ist parametrisierbar – die Feinabstimmung von Prä­zision und Rechenaufwand kann vom Benutzer frei gewählt werden. Der für die Analyse verwendete Abstraktions­grad kann individuell an die Struktur des zu analysierenden Programms angepaßt werden.

  • modular

    Astrée besteht aus verschiedenen Modulen, den sogenannten abstrak­ten Domains. Diese Module können so aktiviert und parametrisiert werden, daß anwendungs­spezifische Analysatoren entstehen, die voll­ständig an eine bestimmte Anwendungs­klasse oder spezifische Be­nutzer­anforderungen angepaßt sind.

    Zur besseren Unterstützung spezifischer Anwendungsklassen kann Astrée durch die Einführung zusätzlicher Module erweitert werden, die die Präzision der Analyse erhöhen.


Jetzt kostenlos testen

Wenn Sie Astrée an Ihren eigenen Anwendungen ausprobieren möchten, nehmen Sie Kontakt mit uns auf.

Release-Notes (Englisch)

Hoch