Wie funktioniert Astrée?

Aufbau

Astrée besteht aus zwei Teilen:

1. dem Astrée-Klienten, mit dem Sie eine Analyse aufsetzen und sich die Ergebnisse anschauen können,
2. dem Analyseserver, auf dem die eigentliche Analyse läuft (oder auch mehrere Analysen, jede als ein eigener Prozeß).

Der Klient bietet sowohl eine gra­phische Benutzer­obefläche als auch Batchmode-Betrieb zur ein­fachen Automati­sierung und Integration.

Beide Teile können auf demselben Rechner laufen. Typischerweise läuft der Server jedoch auf einem leistungs­fähigeren Remote-Host und die Klienten auf den Rech­nern der ein­zelnen Entwickler und Ab­teilungsleiter.

Ihre Lizenzdatei entscheidet darüber, wieviele Klienten zeitgleich auf den Server zugreifen dürfen und wieviele Analyse­prozesse dort parallel laufen können.

Ihre Eingaben

1. Astrée arbeitet auf präprozessiertem C-Code. Auf Wunsch spart Ihnen der eingebaute Präprozessor diesen Arbeitsschritt. Anschließend wird der prä­prozessierte Code geparst und in eine Zwischen­darstellung für die Analyse über­setzt.

2. Für jede Analyse können Sie einen eigenen Eintrittspunkt angeben – meistens ist das eine Funktion von besonderem Interesse für Sie, oder einfach nur main. Astrée analysiert dann sämtliche Code­abschnitte, die von diesem Eintritts­punkt aus durch ununter­brochene sequen­tielle Programm­ausführung erreich­bar sind.

3. Sie können einen Analyse-Wrapper aufsetzen – z. B. um reaktives System­verhalten zu modellieren. Der Wrapper wird als eine eigen­ständige C-Datei in die Ana­lyse ein­gebunden.

4. Astrée kann ferner mit verschiedenen Einstellungen der Appli­cation–Binary-Schnittstelle (ABI) konfi­guriert werden.

5. Zuletzt können Sie Astrée Zusatz­informationen zur Verfügung stellen, z. B. um die Aus­führungs­umgebung zu beschreiben oder die Präzision der Analyse zu steuern. Das erfolgt in einer separaten Datei, sodaß Ihr Quellcode nicht angefaßt werden muß.

   Die Zusatzinformationen werden in einem leicht verständlichen Textformat angegeben, der Astrée-Anno­tation-Language AAL, oder einfach mit dem inte­grierten Annotation-Wizard erzeugt. Sie nehmen auf keine Zeilennummern Bezug, sondern auf die eigentliche Programms­truktur, und müssen somit nicht bei jeder Code­änderung angepaßt werden.

Die Ergebnisse

Das wichtigste Ergebnis der Analyse ist eine Liste von Alarmen, sprich von möglichen Laufzeitfehlern. Jeder Fehler wird zusammen mit seinem Typen angegeben sowie der genauen Stelle im Quellcode, an der er auftritt. Wenn Astrée beweisen kann, daß ein Alarm in einem bestimmten Kontext unter allen Umständen auftritt, wird dieser Alarm als ein eindeutiger Laufzeitfehler eingestuft.

Zur schnellen Orientierung wird das Gesamtergebnis in der Benutzeroberfläche mithilfe einer Ampel dargestellt:

rot	mindestens ein Laufzeitfehler
gelb	keine Fehler, aber mindestens ein Alarm vom Typ A
grün und gelb	keine Fehler und keine Alarme vom Typ A, aber mindestens ein Alarm vom Typ C
grün	keine Fehler und keine Alarme
Typ-A-Alarm: ein möglicher Laufzeitfehler mit unvorhersehbaren Auswirkungen Typ-C-Alarm: ein möglicher Laufzeitfehler mit vorhersagbaren Auswirkungen Fehler: entweder ein Typ-A-Alarm, der in einem bestimmten Kontext garantiert auftritt, oder ein fataler Fehler in der Analyse (z. B. durch inkorrekte oder unvollständige Eingaben)

Darüberhinaus stehen Ihnen vielfältige interaktive Detailansichten, Tabellen und Graphen helfend zur Verfügung.

Zusätzlich überprüft der integrierte RuleChecker Ihren Code auf die Einhaltung von MISRA-Regeln und berechnet vielfältige Code-Metriken wie Comment-Dichte und zyklomatische Komplexität.

Ferner kann Astrée benutzerdefinierte Annahmen zu funktionalen Programmeigenschaften überprüfen, ähnlich der „assert“-​Diagnostik. Wird eine Annahme nicht als verletzt gemeldet, gilt die Korrektheit des dazu­gehörigen C-Ausdrucks als bewiesen.

Sollten unentbehrliche Daten fehlen oder uneinlesbar sein, wird die Analyse stets mit einem Fehler abbrechen.

Astrée zeigt Ihnen auch an, wenn bestimmte Codeabschnitte nicht analysiert wurden. Sofern die Analyse keine Laufzeit­fehler gefunden hat, gelten solche Abschnitte als garantiert unerreichbar vom angegebenen Startpunkt aus („toter Code“).

Für Dokumentation und Zertifizierung können detaillierte Analyseberichte gespeichert werden. Ebenso können Sie das gesamte Analyse-Projekt mit allen Dateien, Einstellungen, Ihren Annotationen und Kom­mentaren abspeichern.

Fehlerbehebung

Die gefundenen Laufzeitfehler können Sie in Ihrem Astrée-Klienten interaktiv unter­suchen, mit Kom­mentaren versehen oder gleich im integrierten Code-Editor beheben.

Eventuelle Fehlalarme können Sie mit AAL-Annotationen als solche kennzeichnen, damit sie nicht wieder auftreten. Alternativ können Sie die Analyseeinstellungen anpassen, oder die Analysegenauigkeit an den ge­wünschten Stellen erhöhen.

Danach können Sie die Analyse neu starten und die verbesserten Ergebnisse begutachten.

Bei Bedarf wiederholen Sie diese Schritte, bis keine Alarme mehr vorliegen. Dann ist die Abwesenheit von Laufzeitfehlern in Ihrem Code formal bewiesen.

Konfiguration

Jede Astrée-Analyse kann auf vielfältige Weisen konfiguriert werden:

1. Optionen
   • Einstellungen der Präzision und der abstrakten Domains
   • Aspekte der Semantik
   • Umfang und Detailliertheit der Ausgaben
2. Direktiven
   • semantische Informationen, z. B. Wertebereiche und Invarianten
   • Parameter für lokale Anpassungen der Analysepräzision
3. ABI-Einstellungen
   • Größe der atomaren Typen
   • Alignment-Einstellungen
   • Byte-Reihenfolge
   • Vorzeichen von Char und Bitfield
   • usw.
4. Filter
   z. B. zum Ignorieren von Inline-Assembly oder ungenormten Keywords
5. Wrapper- und Stub-Code