Startseite > Embedded > Entwicklungstools > Statische Analyse im Vergleich

Qualitätssicherung eingebetteter Systeme

Statische Analyse im Vergleich

22. November 2011, 9:53 Uhr | Von Kerstin Hartig, Dr. Jochen Burghardt und Dr. Jens Gerlach

▶ Diesen Artikel anhören

Fortsetzung des Artikels von Teil 1

Werkzeug fürs Abstrakte

Tool	Polyspace	Astrée	Frama-C
Anbieter	MathWorks	AbsInt	CEA-LIST
für Sprache	C, C++, ADA	C	C
Annotationen zur Steuerung der Analyse	nein	ja	ja (ACSL)
nicht-unterstützte Sprachkonstrukte	dynamische Arrays	malloc, Rekursion	dynamische Arrays, malloc, Rekursion
Überprüfung funktionaler Eigenschaften	nein	nein	ja (Jessie-Plug-in)

Tabelle 2: Werkzeuge zur statischen Analyse

Tabelle 2 stellt die gängigsten Werkzeuge gegenüber, die abstrakte Interpretation für die Detektion von Laufzeitfehlern einsetzen. Eines der ersten und dadurch bekanntesten Werkzeuge ist »Polyspace« von Mathworks, das nach der durch einen Softwareüberlauf verursachten Explosion einer Ariane-Rakete im Juni 1996 entwickelt wurde. »Astrée« von AbsInt ist von den betrachteten Werkzeugen das schnellste und durch seine ausgeklügelten Voreinstellungen sehr präzise.

Die abstrakte Mengenrepräsentation und zahlreiche andere Einstellungen kann der Benutzer an das analysierte Programm anpassen. Somit steigt die Analysegenauigkeit, und der Anteil an falschen Alarmen sinkt. Zusätzlich lässt sich bei Astrée mittels Annotationen des zu analysierenden Quellcodes die Präzision zielgenau erhöhen. Während für Polyspace und Astrée nicht unerhebliche Lizenzkosten anfallen, kann das quelloffene Werkzeug »Frama-C« prinzipiell kostenlos benutzt werden.

Anbieter CEA-LIST bietet aber auch kostenpflichtigen Support an. Frama-C bietet eine modulare Plug-in-Architektur und ermöglicht verschiedene Analyseverfahren für die Programmiersprache C. Die Erkennung von Laufzeitfehlern mittels abstrakter Interpretation unterstützt das Plug-in »Value-Analysis«. Bei Frama-C kann der Anwender ebenfalls Anweisungen an den Analyzer im Quellcode hinzufügen, das Tool benutzt hierbei die Spezifikationssprache »ACSL« (ANSI/ISO-C Specification Language).

Mit diese Sprache lassen sich auch funktionale Eigenschaften in Form von Funktionsverträgen mit Vor- und Nachbedingungen beschreiben, die sich über die Steuerung des Value-Analysis-Plug-ins hinaus auch für eine deduktive Verifikation verwenden lassen. Die vorgestellten Werkzeuge kamen und kommen in industriellen Anwendungen zum Einsatz, etwa der Analyse von Software in der Automobilindustrie, im Bahnbereich und in der Luft- und Raumfahrt.

Fraunhofer FIRST berät bei der Planung und Durchführung statischer Analysen zur Qualitätssicherung eingebetteter Systeme. Die Bedienung dieser Analysewerkzeuge, insbesondere die Nachbearbeitung, ist nicht trivial und erfordert ein nicht zu unterschätzendes Maß an Erfahrung. Falsche Alarme zu eliminieren stellt hierbei die größte Herausforderung dar.

Zusätzlich müssen bei der Verwendung der Werkzeuge etwaige Einschränkungen in den Programmierrichtlinien berücksichtigt oder kreative Lösungen gefunden werden, um beispielsweise rekursive Aufrufe oder dynamische Speicherverwaltung zu ermöglichen. Als Lohn für diesen Aufwand erhält der Anwender jedoch eine zuverlässige Aussage über die Abwesenheit von Laufzeitfehlern. Eine solche Aussage lässt sich leider nicht mit weniger Aufwand erbringen.

Über die Autoren:

Kerstin Hartig ist wissenschaftliche Mitarbeitern, Dr. Jochen Burghardt ist wissenschaftlicher Mitarbeiter und Dr. Jens Gerlach ist Forschungsleiter Verifikation, alle bei Fraunhofer FIRST.