Contract Based Testing für Embedded-Systeme

Anbieter zum Thema

Parasoft® Deutschland GmbH

RTI Real-Time Innovations

protos software gmbh

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.

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

• 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

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 mit Hilfe von Asserts. 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.

Contract-Erweiterungen

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 Statemachines. Reihenfolgen und zeitliches Verhalten (temporale Logik) von synchronen oder asynchronen Aufrufen können damit sehr exakt spezifiziert werden. Außerdem sind Statemachines eine Methode, die den meisten Embedded-Entwicklern bekannt ist.

Die Interface Statemachine 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 (Bild 3) zeigt die Spezifikation aller erlaubten Aufrufe an einer einfachen Schnittstelle als Interface Statemachine. Nur auf Grund 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 Statemachine, 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. 10 hoch 12 auf 300.000.

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 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-Statemachine. Während der Modellierung werden die Implementierungs-Statemachines 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.

Der Hauptvorteil ist die frühe Erkennung und Behebung von Bugs 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 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 Sequenzdigramms mit der Fehlerursache und dem exakten Ablauf rund um das Fehlverhalten

Im folgenden Beispiel hat der aus dem Contract generierte Monitor zur Laufzeit ein Fehlverhalten entdeckt. Im generierten Sequenzdiagramm sieht man den exakten Zeitpunkt, 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 zur Testzeit (Test-Case-Generierung)

Zur Generierung von Test Cases sind die Interface Statemachines im Allgemeinen nicht sehr gut geeignet, da sie keine Aussagen über das Gesamtverhalten eines Systems under Test (SUT) machen.

Statt der Interface Statemachines verwenden wir in der Test Sprache 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.

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.

Zusammenfassung

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

(Der Beitrag wurde mit freundlicher Genehmigung des Autors dem Embedded Software Engineering Kongress Tagungsband 2019 entnommen.)

Der Autor

Thomas Schütz studierte Luft- und Raumfahrttechnik in München und gründete 1997 die PROTOS Software GmbH. Als Softwareprojektleiter oder Architekt konnte er seine Erfahrung in der Verbindung modellbasierter Ansätze mit den Anforderungen von Embedded Systemen in zahlreiche Projekte einbringen. Thomas Schütz berät Firmen beim Aufbau von domänenspezifischen Werkzeugketten und Testsystemen für Embedded Systeme und ist Projektleiter des Eclipse Projektes eTrice.

Boeing-Crash: „Haben Sie Ihre Zustände nicht im Griff, fliegt Ihnen das System um die Ohren“

Grundlagen des Modellbasierten System-Engineering (MBSE)

(ID:46517633)