Schnelle und sichere statische Analyse

Astrée ist:

• sicher
• automatisch
• schnell
• anpassungsfähig
• parametrisierbar
• modular
• präzise
• aktuell

• sicher

  Die meisten Tools auf dem Markt berück­sichtigen nicht alle möglichen Laufzeit­fehler. Viele melden ganz bewußt nur 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. Zum Erfül­len der aktuellen Sicherheits­standards wie ISO 26262, DO-178B/C, IEC-61508 oder 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ö­tigt Astrée zur Analyse von Flug­steuerungs­software mit 132 000 Zeilen C-Code selbst auf einem Single-Core-2,8-GHz-PC lediglich 80 Minuten. Schnellere Rechner liefern entsprechend schnellere Ergebnisse. Multicore-Hardware und verteilte Verarbeitung werden unterstützt.

• 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 jeweilige Anwendungs­klasse angepaßt werden, um deren spezifische Eigen­schaften zu berück­sichtigen, was zur Durch­führung komplexer Beweise unerläßlich ist. Beispiels­weise berück­sichtigt 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 weiter 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 ist es sogar in der Lage, mit nur wenigen Zusatz­einstellungen oder 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 Produktupdate. Jeder Kunde, egal mit welcher Lizenz, bekommt mindestens ein Update völlig kostenlos und automatisch zugeschickt. Und unsere Kundenbetreuung hört sich Ihre Wünsche und Verbesserungsvorschläge nicht bloß an, sondern sorgt auch dafür, daß sie umgesetzt werden.