German Title: Contract Tests für zuverlässige eingebettete Systeme

Preview

PDF, English (PhD Thesis) - main document Download (3MB) | Terms of use

Abstract

Embedded systems comprise diverse technologies complicating their design. By creating virtual prototypes of the target system, Electronic System Level Design, the early analysis of a system composed by electronics and software is possible. However, the concrete interaction between hardware modules and between hardware and software is left for late development stages and real prototype making. Generally, interaction between components is assumed to be correct. However, it has to be assumed on development implicitly because interaction between components is not considered in the functionality design.

While single components are mostly thoroughly tested and guarantee certain reliability levels, their interaction is based on often underspecified interfaces. Although component usage is mostly specified, operational constraints are often left out. Finally, not only the interaction between components but also with the environment and the user are not ensured. Generally, only functional integration tests are executed and corner-cases are left out, leaving uncovered faults that only manifest as failures later when their cost is higher. Therefore, this work aims at component interaction through specification of interfaces, test generation and real-time test execution. The specification is based on the design-by-contract approach of software that specifies semantics of component interaction in addition to the syntactical definition through functions.

In the first part of this work, a specification for the interaction between hardware modules is given. With the automatic real-time test execution, fulfillment of specified preconditions for correct component operation can be checked. In component-based design, the component is trusted and thus, its functionality is assumed to be correct when certain postconditions are specified. In a correct component assembly, component postconditions fulfill preconditions of other components resulting in an operational system.

The specification of preconditions follows the definition of environmental properties, acceptable input sequences for interfacing pins, as well as acceptable signal parameters, such as voltage levels, slope times, delays and glitches. Postconditions are defined by the description of a functionality accompanying constraints, such as timing. These parameters are automatically determined on operation by a testing circuit. Parameters that violate the specification are signaled by the testing circuit and failure is detected. The chosen parameters can give hint of the reason for the failure being an evidence of a circuit fault. In the example of an Inter-Integrated Circuit (I2C) communication system, we define contracts and show comparisons between contract violation, fault categorization and failure occurrence under signal fault injection.

To complete this work, support for fault analysis on the electronic system level design is given. For this, the data transfers between the high-level models used in the design are augmented with the defined contract parameters. With a specific interface, digital faults are generated for transactions with violating signal parameters that can be tracked by the system. This way, recovery mechanisms for synchronous communication are proposed and tested.

In the second part, the interaction between hardware and software is tackled providing special methods for developing device drivers. For this, we do not only specify the interface between hardware and software but also map the hardware control elements to software, partially generating the software interface for a device. This is necessary because drivers handle devices with internal control elements like registers, data streams and interrupts that cannot be represented on software.

This systematic composition of drivers facilitates the development of a device interface called the device mechanism. It is the lowest layer of a two-layer architecture for driver development. The device mechanism carries out the access to the device exporting a pure software interface. This interface is based on the device implementation being, thus, fully specified. Further data processing required for compliance with the operating system or application is carried out in the driver policy, the layer on top of it.

With the definition of a software layer for device control, contracts specifying constraints of this interface are proposed. These contracts are based on implementation constraints of the device and on its dynamic behavior. Therefore, an extended finite state machine models the dynamic behavior of the device. Based on it, functions of the device mechanism can be augmented with preconditions on the state or on state machine variables. These conditions are then checked on runtime. After execution of a function, its postconditions are ensured, such as timing. This guarantees that different driver policies, operating systems or firmwares, use this same device mechanism fulfilling its constraints. On the example of a Philips webcam, we develop the complete driver for Linux based on our architecture, creating contracts for its device mechanism. Following the systematic composition and the contract approach, driver bugs are avoided that otherwise violate allowed values for device data and execution orders of device protocols.

Translation of abstract (German)

Eingebettete Systeme umfassen unterschiedliche Technologien, was ihren Entwurf erschwert. Durch Erstellen eines virtuellen Prototyps vom Zielsystem mittels Electronic System Level (ESL), wird die frühzeitige Analyse von einem System aus Software und Elektronik ermöglicht. Jedoch wird das konkrete Zusammenspiel zwischen Hardwaremodulen beziehungsweise zwischen Hardware und Software erst in den späteren Entwicklungsphasen und in der Prototyperstellung deutlich. Selbst in diesen Entwicklungsphasen liegt das Hauptaugenmerk auf der Systemfunktionalität. Dabei rückt die Sicherstellung des richtigen Zusammenspiels in den Hintergrund, obwohl das für die Systemfunktionalität erforderlich ist.

Während einzelne Komponenten ausführlich getestet werden, wodurch eine gewisse Zuverlässigkeit eingehalten wird, werden ihre Schnittstellen nicht ausführlich genug spezifiziert. Folglich wird weder die korrekte Interaktion zwischen Komponenten noch zwischen einer Komponente und ihrer Umgebung bzw. ihrem Benutzer gewährleistet. Im Normalfall werden sie nur funktional getestet. Das lässt Defekte länger unentdeckt, was höhere Kosten verursacht, denn die Fehlerbeseitigung ist umso teuerer, je später Fehler entdeckt werden. Deshalb zielt diese Arbeit darauf ab, eine richtige Komponenteninteraktion durch die Spezifikation von Schnittstellen, die Testgenerierung und die Testausführung in Echtzeit zu gewährleisten. Die Spezifikation basiert auf dem Design-by-Contract-Ansatz von Software, der die Semantik der Komponenteninteraktion spezifiziert.

Im ersten Teil dieser Arbeit wird eine Spezifikation für das Zusammenspiel zwischen Hardwaremodulen präsentiert. Mit der automatischen Testausführung in Echtzeit können die Vorbedingungen für den richtigen Komponentenbetrieb überprüft werden. Im komponentenbasierten Design werden die Komponenten als fehlerfrei betrachtet. Dennoch weist die Ausführung der Funktionalität Verhaltenseigenschaften auf, durch die Nachbedingungen definiert werden, z.B. zeitversetzte Ergebnislieferung. In einer korrekten Komponentenzusammenstellung ergibt sich ein betriebsfähiges System aus Komponenten, deren Verhalten die Vorbedingungen anderer Komponente einhalten.

Die Spezifikation von Vorbedingungen folgt der Definition von Umgebungseigenschaften, zulässigen Eingangsreihenfolgen für Schnittstellenpins sowie zulässigen Signalparametern, wie Spannungspegeln, Flanken, Verzögerungen und Glitches. Diese Parameter werden während des Betriebs von einer Testschaltung ermittelt. Befinden sie sich außerhalb der definierten Grenzen, werden sie als fehlerhaft markiert, wodurch ein möglicher Ausfall erkannt wird. Anhand des Beispieles eines Inter-Integrated Circuit (I2C) Kommunikationssystems wird sein Contract definiert und die Parallele zwischen den Verstößen gegen den Contract, der Defektkategorisierung und dem Ausfall aufgrund von Fehlereinspeisungen gezeigt.

Um die Arbeit an Hardware-Contracts zu vervollständigen, wird die Fehleranalyse mit dem ESL-Design ermöglicht. Die Datenübertragungen zwischen den ESL High-Level-Modellen werden mit den definierten Contract-Parametern erweitert. Somit können anhand einer spezifischen Schnittstelle digitale Fehler für Übertragungen mit den vom Contract abweichenden Signalparametern generiert werden. Diese Fehler können dann bei der Simulation des ESL-Designs zurückverfolgt werden. Auf diese Weise werden fehlerkorrigierende Maßnahmen für eine synchrone Kommunikation vorgeschlagen und ausgewertet.

Im zweiten Teil der Arbeit wird das Zusammenspiel zwischen Hardware und Software durch spezielle Methoden zur Treiberentwicklung angegangen. Nicht nur wird die Schnittstelle dazwischen spezifiziert, sondern es werden auch die Steuerelemente der Hardware in der Software abgebildet, so dass eine Softwareschnittstelle zum Gerät partiell generiert werden kann. Das ist notwendig, denn die Treiber handhaben Geräte durch Steuerelemente, wie Register, Datenströme und Interrupts, die in der Software nicht vorhanden sind.

Der systematische Aufbau von Treibern vereinfacht die Entwicklung einer Geräteschnittstelle namens Device Mechanism. Sie ist die untere Schicht einer Zweischicht-Architektur für die Treiberentwicklung. Der Device Mechanism bietet eine reine Softwareschnittstelle zum Gerät an. Im Gegensatz zu einem kompletten Treiber nimmt er nur die Geräteansteuerung vor, ohne selbst die Daten zu verarbeiten. Indem der Device Mechanism die Funktionalität mit der Geräteimplementierung teilt, ist er vollständig spezifiziert. Darauf baut eine weitere Schicht namens Driver Policy auf. Diese vervollständigt die Datenverarbeitung indem sie den Betriebssystemanforderungen genügt.

Auf der Basis des Device Mechanisms werden Contracts für die Spezifikation der Schnittstellen eingesetzt. Dafür wird das dynamische Verhalten des Gerätes durch eine erweiterte Zustandsmaschine modelliert. Darauf basierend können die Funktionen des Device Mechanisms um Vorbedingungen an den Zustand oder an die Variablen der Zustandsmaschine erweitert werden, die während der Laufzeit überprüft werden. Nach Ausführung einer Funktion wird für die Einhaltung ihrer Nachbedingungen gesorgt. So kann die Einhaltung der Rahmenbedingungen bei der Benutzung von verschiedenen Driver Policies, für Betriebssysteme oder Firmwares, gewährleistet werden, die sich einen universellen Device Mechanism teilen können. Nach diesem Prinzip wird ein Linux-Treiber für eine Philips Webcam entwickelt. Das Konzept kann Treiberfehler vermeiden, die auf falsche Interpretationen von Gerätedaten oder nicht vorgesehene Bedienungsabläufe zurückzuführen sind.