Call for Papers

ESE-Kongress 2009

Der statische Analysator Astrée ( Vortrag )

Referent: Dr. Daniel Kästner , AbsInt GmbH
Vortragsreihe: Test & Qualität
Zeit: 10. Dezember 16:45

Zielgruppe

Entwicklung, Fortgeschrittene

Themenbereiche

Implementierung, Test & Qualitätssicherung, Sichere Software

Kurzfassung

Sicherheitskritische eingebettete Systeme müssen hohen Qualitätsanforderungen genügen. Laufzeitfehler, z.B. arithmetische Überläufe oder Rundungsfehler können zu fehlerhaftem Programmverhalten führen; ein solcher Fehler führte z.B. zur Explosion der Ariane 5. Da in der Regel keine vollständige Testabdeckung möglich ist, werden zunehmend statische Verfahren eingesetzt. Statische Analysatoren bieten 100% Coverage; um akzeptable Analysezeiten zu erreichen, nehmen statische Analysatoren jedoch in Kauf, dass es zu Fehlalarmen kommt. Da jede Fehlermeldung manuell vom Benutzer überprüft werden muss, kann eine hohe Zahl von Fehlalarmen dazu führen, dass echte Fehler übersehen werden. Der statische Analysator Astrée kann durch Spezialisierung und Parameterisierung exakt an die zu analysierende Software angepasst werden. Dies ermöglicht kurze Analysezeiten und eine niedrige Zahl von Fehlalarmen. Astrée wird z.B. zur Zertifizierung von industrieller Flugzeugsteuerungssoftware eingesetzt.

Nutzen und Besonderheiten

Der Vortrag beschreibt die Funktionsweise statischer Analysatoren und stellt sie klassischen Testverfahren gegenüber. Die Ursachen für Fehlalarme bei statischen Analysatoren werden erläutert, und die Notwendigkeit der manuellen Überprüfung jedes potentiellen Fehlers erklärt. Da viele Softwarewerkzeuge eine hohe Anzahl von Fehlalarmen erzeugen, werden derartige Tools in der Industrie oft nur zur Fehlersuche, aber nicht zum Nachweis der Abwesenheit von Laufzeitfehlern eingesetzt. Im Vortrag werden die im statischen Analysator Astrée verwendeten Techniken zum Erreichen einer hohen Analysepräzision bei niedrigen Laufzeiten erläutert. Unter Bezugnahme auf Astrée wird eine Methodik vorgestellt, einen echten Nachweis der Abwesenheit von Laufzeitfehlern zu führen. Auf diese Weise kann die Sicherheit der eingebetteter Software verbessert werden und gleichzeitig der Validierungsaufwand reduziert werden.

Über den Referenten

Dr. Daniel Kästner studierte Informatik und Wirtschaftswissenschaften an der Universität des Saarlandes und promovierte im Jahr 2000. Er ist Mitgründer und CTO der Firma AbsInt Angewandte Informatik GmbH. Dr. Kästner war Gastdozent an der Universität des Saarlandes und Mitglied in Programmkomittees zahlreicher internationaler Konferenzen. Seine Arbeitsgebiete sind Validierung von Echtzeitsystemen, Compilerbau, sowie Codeoptimierung und Programmanalysen für eingebettete Prozessoren.