Contract-Based-Testing für Embedded Systeme

Das Testen von Embedded Systemen wird mit zunehmender Komplexität erheblich schwerer. Die Methode des Contract-Based-Design eröffnet eine neue Perspektive und sehr effektive Vorgehensweisen, wenn man sie erweitert und auf Tests anwendet.

Was ist der Zweck von Tests?

Testen wird häufig reduziert auf das Entwickeln und Durchführen manueller oder automatisierter Testabläufe. Betrachten wir zunächst die wesentlichen Ziele von Tests:

  • Bewertung der Funktionalität und Qualität eines Systems
  • Erkenntnisgewinn zur Behebung oder Vermeidung von Fehlern

Wir erweitern den Begriff des Tests daher auf alle Methoden, welche diese beiden Ziele unterstützen. Dies können z.B. auch Reviews, formale Verifikation oder Laufzeitmonitoring sein.

Die Herausforderung beim Testen

Um die Ziele zu erreichen, müssen vor allem drei Fragen beantwortet werden:

  • Wie spezifiziert man das geforderte oder verbotene Verhalten eindeutig und hinreichend vollständig?
  • Wie erzeugt man daraus Prüfungen, die mit hoher Wahrscheinlichkeit bereits während der Entwicklung fehlerhaftes Verhalten entdecken?
  • Wie findet man Fehler, die erst beim Einsatz des Systems auftreten, z.B. durch fehlerhafte Verwendung oder Umgebungsbedingungen?

In vielen Fällen kann man diese Fragen recht elegant durch den Einsatz von Contracts beantworten.

Klassische Contracts nach Bertrand Meyer

Design by Contract (DbC) wurde entwickelt und eingeführt durch Bertrand Meyer. DbC erlaubt die Definition formaler Verträge für Schnittstellen und Verhalten von Software-Komponenten. Pre- und Post-Conditions, Invarianten und Seiteneffekte definieren die Semantik von Funktionen. Sprachen wie Ada und Eiffel unterstützen die Definition und Validierung von Contracts.

Hier ein Beispiel für die Umsetzung eines sehr einfachen Contracts mit Pre- und Post-Conditions in der Sprache C mithilfe von Asserts.

Kontrakt im C-Code

Diese Art von Contracts wird auf der Komponentenebene definiert, also für Schnittstellen von Funktionen, Klassen oder C-Modulen. Die daraus resultierenden Prüfungen können daher auch nur auf dieser Ebene erfolgen. Für Prüfungen zur Designzeit benötigt man die Unterstützung der Sprache (z.B. Ada und Eiffel). Integrations- und Systemtests für Embedded-Systeme sind damit kaum möglich.

Design by Contract

Contract-Erweiterungen für Embedded Systeme

Wir benötigen Erweiterungen der Contracts, die es ermöglichen, asynchrones, nebenläufiges Verhalten für alle Ebenen eines Systems formal zu beschreiben. Eine exzellente Methode hierfür sind Interface State Machines. Reihenfolgen und zeitliches Verhalten (temporale Logik) von synchronen oder asynchronen Aufrufen können damit sehr exakt spezifiziert werden. Außerdem sind State Machines eine Methode, die den meisten Embedded Entwicklern bekannt ist. Die Interface State Machine definiert zu jedem Zeitpunkt welche Aufrufe erlaubt sind. Jeder andere Aufruf ist verboten. Dies reduziert die Anzahl der erlaubten Aufrufreihenfolgen um Größenordnungen. Kann man die Einhaltung des spezifizierten Verhaltens testen oder zur Laufzeit überwachen, führt dies zu erheblich einfacheren Systemen, die wesentlich weniger Fehler enthalten.

Das folgende Beispiel zeigt die Spezifikation aller erlaubten Aufrufe an einer einfachen Schnittstelle als Interface State Machine. Nur aufgrund der C-API kann man z.B. folgende Fragen nicht beantworten:

  • Ist der Aufruf von function1 direkt nach initialize erlaubt?
  • Muss ich nach stop wieder initialize aufrufen?

Spezifiziert man die erlaubte Reihenfolge als Interface State Machine, so kann man die Fragen schnell und eindeutig beantworten:

  • Nach initialize muss man zunächst start aufrufen. Danach ist der Aufruf von function1 erlaubt.
  • Nein, nach stop muss nicht initialize aufgerufen werden. Es darf nur start aufgerufen werden.

Die Anzahl der erlaubten Aufrufreihenfolgen reduziert sich für den einmaligen Aufruf aller Funktionen von 120 auf 6, bei 3 Iterationen bereits von ca. 1012 auf 300.000.

State Machine als Interface Kontrakt

Interface Contracts sind also eine äußerst effektive Möglichkeit formal erlaubtes und verbotenes Verhalten an Schnittstellen auf allen Ebenen zu spezifizieren. Die zu testenden Zustände kann man damit meist um viele Größenordnungen reduzieren. Ein angenehmer Nebeneffekt ist die hervorragende und eindeutige Dokumentation der Schnittstellenabläufe.

Prüfung der Contracts

Die spezifizierten Contracts können zu drei verschiedenen Zeitpunkten überprüft werden:

  • Zur Designzeit (Zeitpunkt der Programmierung oder Modellierung)
  • Zur Testzeit (Zeitpunkt der Durchführung der Unit-, Integrations- und Systemtests)
  • Zur Laufzeit (System im Produktivbetrieb)

Am Beispiel des Open Source Werkzeuges eTrice und der Testsprache CaGe für miniHIL Systeme wird gezeigt, wie solche Prüfungen aussehen können.

Prüfung von Contracts zur Designzeit (Formale Verifikation)

Im Rahmen des Forschungsprojektes Contract Based Modeling & Design (CBMD) wurde das Werkzeug eTrice und die Sprache ROOM (Real-Time Object-Oriented Modeling) um Contracts erweitert. Die Methoden werden bereits in der Praxis eingesetzt. Im folgenden Beispiel wird die Schnittstellenspezifikation der Ports (fct und terminal) zwischen den Komponenten (Strukturmodell) um einen Contract (Interface Statemachine) erweitert. Die Aktoren enthalten jeweils ein Modell ihres Verhaltens als Implementierungs-State-Machine. Während der Modellierung werden die Implementierungs-State-Machines laufend gegen den Contract geprüft. Verstöße gegen den Contract werden im Modell angezeigt. Die Generierung der Implementierung aus dem Modell stellt sicher, dass das korrekte Verhalten des Modells auch im Code umgesetzt wird.

Interface State Machine - formale Verifikation

Der Hauptvorteil ist die frühe Erkennung und Behebung von Fehlern und potenziellen Problemen. Durch die formale Verifikation werden viele Probleme entdeckt, die durch Tests sehr schwer zu finden sind. Ein Beispiel sind Race Conditions, die zu sporadisch auftretenden, unklaren und kaum reproduzierbaren Fehlersituationen führen.

Eine Einschränkung der formalen Verifikation ist, dass man ein formales Applikationsmodell benötigt, um es zu prüfen. Wird die Applikation nicht modelliert, sondern mit einer Programmiersprache wie C implementiert, so ist die formale Verifikation nur schwer zu realisieren.

Prüfung von Contracts zur Laufzeit (Monitoring)

Ein weiteres Ergebnis des CBMD Projektes ist die Generierung von Contract Monitoren in eTrice/ROOM Modellen. Diese Monitore werden in die Kommunikationsverbindung zwischen den Komponenten oder zu anderen Systemen eingebaut und erlauben die Prüfung von Contracts zur Laufzeit. Hierfür sind folgende Teilfunktionen nötig:

  • Monitoring: Entdeckung des Fehlverhaltens zur Laufzeit
  • Filterung und Eindämmung: Aktion zur Verhinderung von Fehlverhalten, z.B. durch Verhinderung oder Korrektur des fehlerhaften Aufrufs an der Schnittstelle oder die Umschaltung in einen sicheren Zustand
  • Analyse der Ursache und Debugging: Logging eines Sequenzdiagramms mit der Fehlerursache und dem exakten Ablauf rund um das Fehlverhalten
Interface State Machine zur Beschreibung eines Kontrakts

Im Beispiel hat der aus dem Contract generierte Monitor zur Laufzeit ein Fehlverhalten entdeckt. Im generierten Sequenzdiagramm sieht man den exakten Zeitpunkt, den Verlauf und die Ursache.

Die entstehenden Systeme sind sehr robust gegen Fehlverhalten an den Schnittstellen. Dies ist ein entscheidender Vorteil auch bei Systemen, die Safety oder Security Anforderungen haben. Ein Vorteil des Laufzeit-Monitorings ist, dass man auch Applikationen und Schnittstellen, die nicht modelliert wurden, sehr gut mit Monitoren verbessern kann.

Prüfung von Contracts zur Testzeit (Test Case Generierung)

Zur Generierung von Test Cases sind die Interface State Machines im Allgemeinen nicht sehr gut geeignet, da sie keine Aussagen über das Gesamtverhalten eines Systems under Test (SUT) machen. Statt der Interface State Machines verwenden wir in der Testsprache CaGe daher State-Transition-Tests. Mit State-Transition-Tests kann man das erwartete Black Box Verhalten (Contract) eines SUT als State-Transition-Diagramm beschreiben. Daraus können kombinatorische Test Cases generiert werden, welche mit sehr hoher Abdeckung die erlaubten und verbotenen Pfade im SUT testen. Ebenso kann man damit die Datenkombinatorik z.B. für Aufruf- oder Konfigurationsparameter testen.

Verhaltenskontrakt - generierte Test-Cases

State-Transition-Testing ist eine effektive Methode um schnell und strukturiert zu hohen Testabdeckungen zu kommen. Für kleinere Probleme oder geringere Testabdeckungen kann man mit Stift und Papier Test-Cases ableiten und die Tests manuell implementieren. Für größere Abdeckungen ist es sinnvoll, Werkzeuge mit Test-Case-Generator zu verwenden.

Was also bringen Contracts für die Tests?

Erweiterte Contracts …

  • ermöglichen die formale Spezifikation von Schnittstellen nicht nur auf Komponenten-, sondern auch auf Integrations- und Systemebene
  • sind verwendbar für synchrone und asynchrone Systeme (Embedded Systeme)
  • erlauben die exakte Spezifikation von Abläufen und zeitlichen Bedingungen
  • können in allen Entwicklungsphasen zur Verifikation verwendet werden (Design-, Test-, Laufzeit)
  • ermöglichen für viele Bereiche eine sehr hohe Abdeckung
  • können für automatische Generierung von Testfällen und Monitoren verwendet werden

Literatur- und Quellenverzeichnis