High Integrity Systeme

Mit formaler Verifikation gegen Laufzeitfehler

11.05.2010 | Autor / Redakteur: Jay Abraham* / Martina Hafner

Das Problem von High Integrity Systemen: Die z.B. in medizinischen Geräten enthaltene Embedded Software wird zunehmend anspruchsvoller und komplexer. Moderne Schrittmacher etwa können bis zu 80.000 Zeilen Programmcode enthalten,
Das Problem von High Integrity Systemen: Die z.B. in medizinischen Geräten enthaltene Embedded Software wird zunehmend anspruchsvoller und komplexer. Moderne Schrittmacher etwa können bis zu 80.000 Zeilen Programmcode enthalten,

Anhand des Werkzeugs PolySpace wird im Folgenden erklärt, wie ein Tool so helfen kann, Laufzeitfehler wie Überläufe, Divisionen durch Null, Array-Zugriffe außerhalb gültiger Bereiche usw. aufzuspüren oder deren Abwesenheit zu beweisen. Polyspace ist ein Code-Verifikationsprodukt von The MathWorks, das sich der abstrakten Interpretation bedient. Den Input für PolySpace bildet C-, C++- oder Ada-Quellcode. Der Output besteht aus vierfarbig markiertem Quellcode. PolySpace informiert den Anwender mit Hilfe einer Farbcodierung über die Qualität des Codes

  • Grün: Code ist korrekt und zuverlässig
  • Rot: fehlerhafter Code, der Laufzeitfehler auslöst
  • Grau: toter oder unerreichbarer Code
  • Orange: unbewiesener, potentiell unsicherer Codeabschnitt

Die folgende Übung demonstriert die Effektivität der abstrakten Interpretation mit PolySpace. Es sei folgende Funktion angenommen:

1 int where_are_errors(int input)

2 {

3 int x, y, k;

4

5 k = input / 100;

6 x = 2;

7 y = k + 5;

8 while (x < 10)

9 {

10 x++;

11 y = y + 3;

12 }

13

14 if ((3*k + 100) > 43)

15 {

16 y++;

17 x = x / (x - y);

18 }

19

20 return x;

21 }

Das Ziel besteht darin, Laufzeitfehler in der Funktion where_are_errors() zu finden. Die Funktion führt verschiedene mathematische Berechnungen aus und enthält eine while-Schleife sowie eine if-Anweisung. Man beachte, dass alle Variablen initialisiert sind und verwendet werden. In Zeile 17 könnte eine Division durch Null auftreten, falls x = y wird.

Bild 5: Ergebnisse des Verifikationstools Polyspace für die Funktion where_are_errors. Das Ergebnis zeigt, dass es in diesem Code keine Laufzeitfehler gibt.
Bild 5: Ergebnisse des Verifikationstools Polyspace für die Funktion where_are_errors. Das Ergebnis zeigt, dass es in diesem Code keine Laufzeitfehler gibt.

Erlauben aber die eingesetzten Steuerstrukturen und die an x und y durchgeführten mathematischen Operationen, dass x = y werden kann? Wie in Bild 5 dargestellt, hat PolySpace bewiesen, dass es in diesem Code keine Laufzeitfehler gibt. Der Grund dafür ist, dass Zeile 17 nur ausgeführt wird, wenn die Bedingung (3 · k + 100 > 43) als true ausgewertet wird.

Weil aber außerdem der Wert von y von dem von k abhängt, ermittelt PolySpace, dass y in Zeile 17 stets größer als 10 ist, wenn x gleich 10 ist. Darum kann in dieser Zeile keine Division durch Null auftreten. Dieses Ergebnis wird effizient und ohne Ausführung, Instrumentierung und Debugging des Codes oder die Erzeugung von Testfällen ermittelt.

PolySpace identifiziert außerdem sämtliche Operationen des Codes, die potenziell einen Laufzeitfehler erzeugen könnten und unterstreicht sie (Bild 5). Im Beispiel sind sämtliche unterstrichenen Passagen grün markiert, weil keine Laufzeitfehler vorhanden sind. In Zeile 17 beweist z.B. die grüne Markierung des ‚/‘-Operators, dass dieser sowohl sicher gegen Überlaufe als auch gegen Divisionen durch Null ist.

*Jay Abraham ist Technical Manager Verification bei The MathWorks

Inhalt des Artikels:

Kommentar zu diesem Artikel abgeben

Schreiben Sie uns hier Ihre Meinung ...
(nicht registrierter User)

Zur Wahrung unserer Interessen speichern wir zusätzlich zu den o.g. Informationen die IP-Adresse. Dies dient ausschließlich dem Zweck, dass Sie als Urheber des Kommentars identifiziert werden können. Rechtliche Grundlage ist die Wahrung berechtigter Interessen gem. Art 6 Abs 1 lit. f) DSGVO.
Kommentar abschicken
copyright

Dieser Beitrag ist urheberrechtlich geschützt. Sie wollen ihn für Ihre Zwecke verwenden? Infos finden Sie unter www.mycontentfactory.de (ID: 341248 / Software-Test & -Betrieb)