Qualitätssicherung eingebetteter Systeme

Statische Analyse im Vergleich

Viele sicherheitsrelevante Eigenschaften eingebetteter Software, wie die definitive Abwesenheit von Laufzeitfehlern oder die Bestimmung der maximalen Laufzeit eines Programmteils, können Tests nur unzureichend nachweisen. Um dennoch überzeugende und kostengünstige Nachweise für solche schlecht testbaren Eigenschaften zu erbringen, existieren verschiedene Methoden zur statischen Analyse von Software, bei denen die zu analysierende Software nicht ausgeführt wird.

Untersuchungsverfahren, bei denen der Prüfling nicht ausgeführt wird, lassen sich gemäß Bild 1 nach den zu untersuchenden Softwareeigenschaften, der Art des Nachweises und den dabei benutzten Methoden klassifizieren.

Fraunhofer FIRST 

Vollbild

Bild 1: Klassifizierung der statischen Analyse

Schliessen

Fraunhofer FIRST

Bild 1: Klassifizierung der statischen Analyse

Aus dieser Klassifizierung wird deutlich, dass »statische Analyse« ein sehr umfassender Begriff ist. Die Norm für Software in Bahnanwendungen (EN 50128) beispielsweise nennt Code-Reviews durch Entwickler als eine Form der statischen Analyse. Mit anderen Worten: Man kann nicht erwarten, dass für die statische Analyse immer Werkzeugen nötig sind oder dass es auch nur Werkzeuge gibt, die alle interessierenden Eigenschaften eines Programms analysieren können.

Das im Folgenden interessierende Teilgebiet statischer Analysemethoden ist in Bild 1 dunkel unterlegt. In diesem Bereich existieren Werkzeuge, die mittels abstrakter Interpretation die Abwesenheit von Laufzeitfehlern in C-Software nachweisen können.

So sollen »Astrée« von AbsInt, der »Polyspace Code Verifier« von MathWorks und »Value-Analysis«, ein Plug-in für das Open-Source-Framework »Frama-C« miteinander verglichen werden.

Was ist abstrakte Interpretation?

Die abstrakte Interpretation arbeitet das zu analysierende Programm symbolisch ab. Statt einzelner Eingabewerte kommen abstrakte Repräsentationen von Mengen möglicher Werte zum Einsatz; im einfachsten Fall hinreichend große Intervalle. Auf diese Weise lässt sich für jede Programmstelle die Gesamtheit der dort möglichen Variablenwerte bestimmen. Das Programm wird also nicht »konkret«, sondern »abstrakt« interpretiert. Damit lassen sich eine Reihe wichtiger Aussagen über so genannte Laufzeitfehler eines Programms machen. Auch unerreichbaren Code kann dieser Ansatz finden.

Tabelle 1 zeigt beispielhaft, welche Laufzeitfehler sich durch welche Wertemengen erkennen lassen.

Aus prinzipiellen Gründen kann eine abstrakte Repräsentation manche Wertemengen nicht exakt darstellen, stattdessen werden sie durch darstellbare Obermengen konservativ approximiert. Dadurch ist sichergestellt, dass eine fehlerhafte Programmstelle nie als fehlerfrei gelten kann. Daher lassen sich zuverlässige Aussagen über die Abwesenheit von Laufzeitfehlern treffen, was allein durch Tests oder Analysewerkzeuge, die auf der Grundlage von Ad-hoc-Heuristiken arbeiten, nicht möglich ist.

Hierin liegt der wesentliche Vorteil von Verfahren, die auf abstrakter Interpretation beruhen. Andererseits kann ein kritischer Wert (etwa Division durch Null) zwar in der approximierenden Obermenge liegen, aber nicht in der tatsächlichen Wertemenge. In diesem Fall meldet die abstrakte Interpretation einen Laufzeitfehler, der in Wirklichkeit gar nicht vorliegt - ein falscher Alarm.

Wenn es gilt, für ein Programm die Abwesenheit von Laufzeitfehlern mit Hilfe eines Werkzeugs nachzuweisen, so sind alle als möglicherweise fehlerhaft gemeldete Stellen nachzubearbeiten, um sie in echte und falsche Alarme aufzuteilen. Diese Arbeit übernimmt in den meisten Fällen die Person, welche die Analyse durchgeführt hat. Im Falle eines echten Alarms müssen die Entwickler die problematische Stelle im Quellcode ändern.

Für einen falschen Alarm dagegen ist zu begründen, warum in Wirklichkeit kein Laufzeitfehler vorliegt. Alternativ kann der Prüfer auch das Werkzeug zu einer genaueren Analyse veranlassen, um den Alarmstatus der betreffenden Stelle korrekt zu erkennen.

Dazu kann der Anwender etwa die abstrakte Mengenrepräsentation verfeinern oder Programmteile mehrfach unter verschiedenen Zusatzannahmen (beispielsweise für positive und nichtpositive Werte getrennt) analysieren lassen. Einige Werkzeuge (Astrée und Frama-C, siehe Tabelle 2) bieten Annotationen, die dem Code an ausgewählten Stellen hinzugefügt werden können, um den Analyseprozess dort gezielt zu beeinflussen.

Fraunhofer FIRST 

Vollbild

Bild 2: Prozessschritte bei der statischen Analyse

Schliessen

Fraunhofer FIRST

Bild 2: Prozessschritte bei der statischen Analyse

Mit solchen Annotationen lassen sich Schleifen ganz oder teilweise abrollen, Arrayelemente separat analysieren oder Analyseinformationen bestimmter Variablen detailliert ausgeben.

Dadurch steigt der Rechenaufwand für die Analyse nur dort, wo es nötig ist.

Der Arbeitsaufwand für die Analyse bestimmt sich hauptsächlich durch die detaillierte Untersuchung der gemeldeten Alarme.

Bild 2 verdeutlicht, dass statische Analyse ein iterativer Prozess ist, der eine enge Zusammenarbeit mit den Entwicklern erfordert.

1. Teil: Statische Analyse im Vergleich
2. Teil: Werkzeug fürs Abstrakte

Weiterführende Links:

• Sicherung der Codequalität: Statische Analyse ergänzt
• electronic displays Conference 2012
• embedded world Conference 2012