Entwicklungswerkzeuge

mbeddr - Embedded-Entwicklung mit erweiterbarem C

| Autor / Redakteur: Bernd Kolb, Markus Völter * / Franz Graser

Zustandsautomaten und Model Checking

Das Verhalten vieler eingebetteter Systeme ist zustandsgetrieben — so auch das unseres Roboters. Dieser soll sich nach Erhalt eines Einsatzbefehls auf den Weg machen und nach Verdächtigen Ausschau halten. Wurde ein solcher entdeckt, soll er diesen verhaften und zurück zur Basisstation fahren. Ein Einsatz kann jedoch zu jedem Zeitpunkt abgebrochen werden.

Zur Modellierung eines solches Verhaltens bieten sich Zustandsautomaten an. Um diese effizient implementieren zu können, bietet mbeddr ein spezielles Sprachkonstrukt für Zustandsautomaten. Bild 6 zeigt, wie das Konstrukt in unserem Beispiel verwendet wird, um das Verhalten des Roboters zu beschreiben.

Zustandsautomaten in mbeddr können mehrfach instanziiert werden. Dies kann zum Beispiel dazu verwendet werden, um dieselbe Implementierung der Zustandsmaschine mehrfach für die Ansteuerung unterschiedlicher Motoren zu verwenden. Es ist möglich Automaten in Komponenten einzubetten und damit das Verhalten dieser zu modellieren. Neben der textuellen Repräsentation wird mbeddr ab etwa Mitte 2013 auch eine graphische Notation für Zustandsmaschinen anbieten. Ab diesem Zeitpunkt wird MPS neben textuellen, mathematischen und tabellarischen Notationen auch Graphik erlauben.

Ein großer Vorteil der Verwendung von Zustandsmaschinen liegt in ihrer guten Verifizierbarkeit. Mittels Model Checking lassen sich unterschiedliche Eigenschaften von Zustandsmaschinen mathematisch beweisen. Für Zustandsmaschinen, die als verifiable markiert sind, überprüft mbeddr beispielsweise automatisch, dass alle Zustände erreichbar sind sowie dass alle Transitionen deterministisch sind. Benutzer können eigene zu beweisende Eigenschaften festlegen. Für fehlgeschlagene Checks bekommt der Nutzer ein Gegenbeispiel, anhand dessen er nachvollziehen kann, unter welchen Umständen eine gewisse Annahme nicht zutrifft (siehe voriges Bild). Ziel von mbeddr ist es dabei, nicht selbst die mathematischen Beweise zu führen. Vielmehr kommen renommierte kostenfreie Tools wie beispielsweise NuSMV zum Einsatz. mbeddr schafft es jedoch, die mächtigen Werkzeuge für Entwickler zugänglich zu machen und die Analyseergebnisse auf verständliche Weise dem Anwender zu präsentieren und ermöglicht damit für viele Entwickler neue Möglichkeiten bei der Qualifizierung von Embedded-Software.

Physikalische Einheiten

Die Verwendung physikalischer Einheiten als Teil von Typen und Literalen vermeidet eine ganze Klasse von Fehlern. Die entsprechende mbeddr-Erweiterung bettet physikalische Einheiten direkt in das C-Typsystem ein und ist insbesondere in der Lage, mit den Einheiten zu rechnen. Die Benutzer der entsprechenden Spracherweiterung können eigene abgeleitete Einheiten definieren sowie Konvertierungsregeln zwischen den Einheiten beschreiben.

Mittels Spracherweiterung lassen sich auch weitere primitive Einheiten definieren, die nicht zwangsläufig etwas mit den vordefinierten SI-Einheiten zu tun haben müssen. In unserem Beispiel ist im Bild 7 zu erkennen, dass die Operationsparameter mit physikalischen Einheiten annotiert wurden. In der Implementierung wurde eine mit einer Zeit-Einheit annotierte Variable durch eine mit einer Distanz-Einheit annotierte Variable geteilt. Das Ergebnis sollte einer Geschwindigkeits-Variable zugewiesen werden.

mbeddr hat das erfolgreich als Typfehler erkannt. Die driveForward-Operation des Interfaces erfordert beim Aufruf als ersten Parameter die Einheit mm. Beim Aufruf verwenden wir den Unit-Cast-Operator, um 15m in mm zu konvertieren. Die Konvertierungsregeln wurden im UnitContainer im unteren Teil des folgenden Bildes hinterlegt. Dort wurde auch mps (meters per second) als neue Einheit definiert.

Produktlinienvariablilität

Die zentrale Herausforderung im Kontext von Softwareproduktlinien besteht in der skalierbarer Umsetzung der Variabilität der einzelnen Produkte innerhalb der Produktlinie.

In unserem Roboter-Beispiel haben wir eine sehr einfache Produktlinie. Wir benötigen zwei Versionen unserer Software: eine zum Test sowie eine weitere, die auf der echten Hardware ausgeführt werden kann.

In C werden Varianten typischerweise mit Hilfe des Präprozessors erzeugt. Er entfernt einzelne Textabschnitte, wenn das betreffende #define nicht vorhanden ist. In mbeddr steht ein besserer Ansatz zur Verfügung, der nicht auf Textebene, sondern auf Strukturebene arbeitet. Beliebige Programmelemente lassen sich mit sogenannten Presence Conditions versehen. Dies sind Boole'sche Ausdrücke über Konfigurationsschalter. Falls während der Generierung ein solcher Ausdruck zu false evaluiert, werden das betreffende Element und alle seine Kinder aus dem Modell entfernt und damit nicht kompiliert.

Dieses Zurechtschneiden des Programmbaumes lässt sich nicht nur im Rahmen der Generierung durchführen, sondern auch im Editor selbst: Programme lassen sich in jeder beliebigen Variante betrachten und bearbeiten. (Bild 8)

Inhalt des Artikels:

Kommentar zu diesem Artikel abgeben

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

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: 38022700 / Embedded Software Entwicklungswerkzeuge)