Schnelle und sichere Laufzeitfehleranalyse

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

Astrée-Screenshot
Astrée-Screenshot

Astrée wird vorrangig zur Analyse von sicherheits­kritischen ein­gebetteten Anwendungen eingesetzt, insbe­sondere in den Be­reichen Luft- und Raumfahrt, Transport, Medizin­technik und Nuklear­anlagen. Grundsätzlich kann es aber auch beliebige C-Programme analysieren, handgeschriebene wie automatisch erzeugte, mit komplexer Speicher­nutzung, dyna­mischer Speicher­allokation und Rekursion.

Welche Laufzeiteigenschaften überprüft Astrée?

Astrée überprüft, ob die C-Sprache korrekt eingesetzt wurde, und sucht nach Laufzeitfehlern in allen möglichen Ausführungsszenarien unter allen möglichen Bedingungen. Dabei meldet es jeden Gebrauch der Sprache, der laut ISO/IEC 9899:1999, der internationalen Norm für C, ein undefiniertes Verhalten aufweist, sowie jeden Verstoß gegen hardwarespezifische Einschrän­kungen der Imple­mentierung.

Im einzelnen meldet Astrée:

Gleitkommaberechnungen werden von Astrée präzise und sicher behandelt. Alle möglichen Run­dungsfehler, sowie alle Kummulativ­effekte, werden stets berücksichtigt. Gleiches gilt für die Werte −∞, +∞ und NaN in allen Berechnungen und Vergleichen.

MISRA und mehr

Mit dem nahtlos integrierten RuleChecker können Sie die Einhaltung von MISRA-, CWE-, ISO/IEC- und SEI-CERT-Regeln überprüfen. Die Checks sind frei kon­figurierbar, jede Regel und sogar einzelne Aspekte bestimmter Regeln können individuell hinzu­geschaltet werden. Das Tool kann auch vielfältige Code-Metriken berechnen (z. B. Comment-Dichte oder zyklomatische Komplexität) sowie um Ihre haus­eigenen Standards erweitert werden.

Wer benutzt Astrée?

  • Luftfahrt

    2003 verifizierte Astrée die Abwesenheit von Laufzeit­fehlern in der pri­mären Flug­kontroll­software des Fly-by-Wire-Systems eines Airbus-Modells. Die Analyse der 132 000 Zei­len C-Code erfolgte voll­automatisch und be­nötigte nur 80 Minu­ten 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). Seitdem wird Astrée von Airbus France zur Analyse der Flug­kontroll­software verschiedener Flugzeug­modelle eingesetzt, darunter des A380.

  • Raumfahrt

    ESA-Logo

    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. Es war die erste voll­automa­tische Kopplung im All, die nicht von einem russischen Raumfahrzeug durchgeführt wurde.

  • Automobilbau

    Der Automobilzulieferer Helbako setzt Astrée in der Entwicklung von Steuerungs­software ein, um die Einhaltung von MISRA-Standards und die Abwesenheit von Laufzeitfehlern nachzuweisen.

  • Kraftwerke

    MTU Friedrichshafen setzt Astrée zum Beweis der Korrekt­heit der Kontroll­software von Notstrom­aggregaten in Kraft­werken ein. Zusammen mit dem dazu­gehörigen Qualifizierungspaket ist Astrée Teil des Zerti­fizie­rungs­prozesses nach IEC 60880.

    AREVA setzt Astrée zur Verifikation sicherheitskritischer Software ihrer Leittechnik-Systemplattform TELEPERM XS ein, welche u. a. für Reaktor­schutz und Reaktor­regelung verwendet wird.

  • Lüftungstechnik

    Ebm-papst, der weltweit führende Hersteller von Elektromotoren und Venti­latoren für Klima­anlagen und Kühl­systeme, setzt Astrée zur fort­laufenden automa­tischen Verifi­zierung sicher­heits­kritischer Kontroll­software ein.


Individuell anpassungsfähig

Tool-Qualifizierung

Wir bieten sogenannte Qualification-Support-Kits für Astrée an, die den Qualifizierungsprozeß nach DO-178B Level A, ISO 26262, IEC 61508 und anderen Sicherheits­standards wesentlich ver­einfachen.

Der Konkurrenz zehn Jahre voraus

Astrée ist:

  • sicher

    Die meisten Tools auf dem Markt berück­sichtigen nicht alle möglichen Laufzeit­fehler. Viele konzentrieren sich ganz bewußt auf die wahr­scheinlichsten. Diese Tools eignen sich höchstens zum Testen, also zum gelegent­lichen Finden einiger Bugs.

    Für die Verifikation, also zum Nachweis der Abwesenheit jeglicher Lauf­zeitfehler, sind solche Bugfinder weder gedacht noch geeignet. Für die Erfül­lung der aktuellen Sicherheits­standards wie ISO 26262, DO-178B, DO-178C, IEC-61508 und EN-50128 reicht das gelegentliche Finden einiger Bugs nicht.

    Astrée-Analysen sind hingegen sicher. Das Tool berücksichtigt stets alle möglichen Laufzeitfehler, und wird niemals einen davon ver­schwei­gen. Beides ist absolut unerläßlich zur Verifi­kation sicherheits­kritischer Software. Zugleich ist Astrée in der Lage, nur wenige bis gar keine Fehlalarme zu produzieren.

  • automatisch

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

    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

    Andere statische Analysatoren benötigen sehr viel Zeit (typischer­weise mehrere Stunden zum Analysieren von 10 000 Codezeilen) oder verbrauchen extrem viel Speicher. Manche terminieren erst nach Tagen mit einem Speicherüberlauf. Manche terminieren gar nicht.

    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 Flug­steuerungs­software eines Airbus-Models mit 132 000 Zeilen C-Code. Seit 2005 kann Astrée auf Multicore-Hardware laufen, was noch schnellere Analysen ermöglicht.

  • anpassungsfähig

    Universelle statische Analysatoren unterstützen alle in der jeweiligen Programmier­sprache geschrie­benen Anwendungen. Sie können nur in dieser Programmier­sprache ausdrückbare Programm­eigenschaften be­rücksichtigen.

    Domain­spezifische statische Analysatoren schränken die Anwendungs­klasse ein, um spezifische Programm­strukturen 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äßlich sind. Beispielsweise berücksichtigt Astrée bei Control/Command-Programmen die logischen und funktionalen Eigen­schaften der Control-and-Command-Theorie.

  • parametrisierbar

    Bei der statischen Programmanalyse gilt es stets, zwischen Analyse­präzision und Rechenaufwand abzu­wägen. Sehr präzise Analysatoren sind in aller Regel sehr langsam, sehr schnelle Analy­satoren – sehr ungenau.

    Astrée hingegen ist parametrisierbar – die Feinabstimmung von Prä­zision und Rechenaufwand kann von Ihnen frei gewählt werden. Der für die Analyse ver­wendete Abstraktions­grad kann indivi­duell an die Struktur Ihres Programms ange­paßt werden.

  • modular

    Astrée besteht aus verschiedenen Modulen, den sogenannten abstrak­ten Domains. Diese Module können so akti­viert und parametri­siert wer­den, daß anwendungs­spezifische Analysatoren entstehen, die voll­stän­dig an eine be­stimmte Anwendungs­klasse oder spezi­fische 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 noch mehr erhöhen.

  • Präzise

    Universal-Analysatoren erlauben nur sehr geringe Präzision im Hinblick auf Fehlalarme. Das Verhältnis von Fehl­alarmen zur Anzahl der C-Basisoperationen im analy­sier­ten Code liegt typischer­weise bei 10–20 %.

    Spezialisierte Analysatoren erreichen bessere Zahlen, 10 % oder weniger. Leider ist im Produktionseinsatz auf industriellen Anwendungen selbst eine Rate von nur 1 % vollkommen inakzeptabel: bei 100 000 Ope­ratio­nen bedeutet sie 1000 Fehlalarme.

    Im Gegensatz dazu ist Astrée dank seiner Modularität und Anpassungs­fähigkeit außerordentlich präzise. Oft genug ist es in der Lage, mit nur wenigen Zusatz­einstellungen oder gar von sich aus genau null Fehlalarme zu erzeugen. Dies wurde immer wieder von der Industrie unter Beweis gestellt, z. B. bei der Analyse primärer Flugsteuerungs­software durch Airbus.

  • aktuell

    Astrée wird ständig weiterentwickelt, auch und gerade im Hinblick auf die neuesten Forschungs­ergebnisse in der theoretischen Informatik. Wir profitieren seit Jahrzehnten von engster Zusammenarbeit mit Forschungsgruppen in Deutschland, Frankreich und Schweden, die weltweit führend auf dem Gebiet der stati­schen Programm­analyse sind.

    Sie finden kein Konkurrenzprodukt, das nicht weit hinterher­hinkt. Viele sind ganz stehengeblieben, oder nehmen seit Jahren nur noch kosmetische Änderungen vor.

    Wir veröffentlichen alle sechs Monate ein neues Astrée-Release. Jeder Kunde, egal mit welcher Lizenz, bekommt mindestens ein Update völlig kostenlos und automatisch zugeschickt. Und unsere exzellente Kundenbetreuung hört sich nicht nur Ihre Wünsche und Verbesserungsvorschläge an, sondern sorgt auch dafür, daß sie umgesetzt werden.


Jetzt testen

Testen Sie Astrée kostenlos und unverbindlich an Ihren eigenen Anwendungen.