mbeddr: Embedded-Entwicklung mit erweiterbarem C

Inhaltsverzeichnis

Was wäre, wenn Sprachen genau so einfach erweiterbar wären wie Programme? Der Artikel zeigt im Kontext eingebetteter Systeme, wie sich mit der IDE mbeddr die Programmiersprache C erweitern lässt.

Entwickler sind es gewöhnt, ihr Programm bei Bedarf einfach unter Verwendung zusätzlicher Bibliotheken zu entwickeln. Diese haben allerdings den Nachteil, dass sie keine domänenspezifische Syntax, statischen Constraints oder Typregeln mitbringen und auch die IDE nicht erweitern. Spracherweiterungen können dieses Manko beheben, und Language Workbenches sind in der Lage, derartige inkrementelle Spracherweiterung umzusetzen. Mit ihnen lassen sich Sprachen effizient entwickeln, kombinieren und verwenden.

Herausforderungen für eingebettete Systeme

Die Entwicklung eingebetteter Systeme stellt die folgenden Herausforderungen an den Entwickler:

• Abstraktionen ohne Laufzeit-Overhead: Gute Abstraktionen führen zu weniger Code und zu besserer Analysier- und Wartbarkeit. In eingebetteten Systemen sind derartige Abstraktionen allerdings mit möglich wenig Laufzeitkosten umzusetzen, da die Ressourcen auf den Zielgeräten üblicherweise beschränkt sind.
• C ist gefährlich: Die verbreitetste Programmiersprache für eingebettete Systeme hat durchaus einige Mängel, die bei Embedded-Systemen zu ernsthaften Problemen führen können. Dazu gehören zum Beispiel Void-Pointer und die unkontrollierte Verwendung des Präprozessors.
• Programm-Annotationen: Programme in technischen Domänen benötigen oft zusätzliche Spezifikationen für Typen oder Variablen. Dazu gehören Größenbeschränkungen, physikalische Einheiten, oder Zugriffsbeschränkungen. Sie lassen sich in C nicht sinnvoll an den entsprechenden Typen oder Variablen anbringen, das Auslagern in XML-Dateien verbessert die Situation ebenfalls nicht.
• Verifikation: Eingebettete Software existiert oft im Kontext sicherheitskritischer Systeme. Dort ist die Software vor dem Einsatz möglichst umfangreich auf Korrektheit zu untersuchen. Die Verifikation von C ist teuer, insbesondere durch die Komplexität und den niedrigen Abstraktionslevel der Sprache.
• Prozessunterstützung: Ein Großteil aller eingebetteter Systeme entsteht im Rahmen von Produktlinien. Um die damit einhergehende Komplexität in den Griff zu bekommen, ist es unter anderem nötig, die Variabilität der Produkte innerhalb der Produktlinie systematisch zu verwalten und eine stringente Nachvollziehbarkeit von den Implementierungsartefakten zu den Anforderungen sicherzustellen.

Mehr Infos

MPS

MPS zeichnet sich unter anderem durch einen projizierenden Editor aus, der, wie für solche Werkzeuge üblich, ohne Grammatik und Parser auskommt. Dadurch lassen sich unterschiedliche Notationen verwenden: Text, Tabellen, Symbole wie Bruchstriche und Grafiken. Außerdem führt das dazu, dass sich Sprachen einfach modularisieren und kombinieren lassen. MPS wird standardmäßig mit Java ausgeliefert, sodass sich auch Java inkrementell erweitern lässt. Außerdem können Entwickler mit MPS separate DSLs bauen. MPS ist derzeit in Version 2.5 verfügbar und steht unter der Apache-2.0-Lizenz. Für 2013 sind die Integration in Eclipse und die Unterstützung grafischer Notationen geplant.

Aufgrund dieser Anforderungen kommen bei der Entwicklung eingebetteter Systeme oft eine Vielzahl von Werkzeugen zum Einsatz. Ihre Integration führt allerdings zu weiteren Herausforderungen.

Der mbeddr-Ansatz

Um diese Probleme in den Griff zu bekommen, unterstützt die IDE mbeddr auf Basis von C inkrementelle, domänenspezifische Spracherweiterungen. Die Technik nutzt JetBrains' Language Workbench MPS (Meta Programming System, die die notwendigen Mechanismen zur Verfügung stellt. mbeddr umfasst eine IDE für C und Erweiterungen. Außerdem stellt es einen erweiterbaren Debugger zur Verfügung. Sowohl mbeddr als auch MPS sind als Open-Source-Software verfügbar.

Spracherweiterung und MPS

Unter Spracherweiterung versteht man das modulare Hinzufügen neuer Sprachkonzepte. Dabei liegt die Betonung auf modular: Die Basissprache, hier C, darf nicht invasiv verändert werden, um neue Sprachmodule hinzuzufügen. Außerdem sollten sich unabhängig voneinander entwickelte Spracherweiterungen nicht gegenseitig stören. Das hat insbesondere zur Folge, dass die Komposition unabhängig entwickelter Syntaxbeschreibungen nicht zu ungültigen Sprachen führen darf. Bei Verwendung klassischer Parsergeneratoren ist das ein Problem, bei projizierenden Editoren tritt das nicht auf.

Neue, typischerweise abstraktere oder domänenspezifische Sprachkonstrukte werden im Rahmen von Transformationen auf existierende Sprachkonstrukte zurückgeführt. Das können entweder Konstrukte anderer Erweiterungen oder der Basissprache C sein. Nach dem Zurückführen aller Erweiterungen auf die Basissprache übersetzt ein gewöhnlicher Compiler das Programm. Bei mbeddr kommt entweder gcc oder ein für die Zielplattform passender Compiler zum Einsatz.

MPS hat sich als geeignet für diese Art der modularen Spracherweiterung herausgestellt. Das liegt vor allem daran, dass MPS ein projizierende Editor ist, wodurch eine Änderung an einem Programm in ihm direkt zur Änderung des abstrakten Syntaxbaums führt. Die Herausforderung, dass der Parser die Struktur des Baums aus der flachen, sequenziellen Textstruktur (re-)konstruieren muss, fällt weg. Außerdem kann die Komposition unabhängig entwickelter Sprachen nie zu ungültigen Sprachdefinitionen führen. Das führt letztlich zu nahezu unbegrenzter Spracherweiterbarkeit. Des Weiteren sind projizierende Editoren nicht auf textartige Syntaxformen beschränkt. Tabellarische, mathematische oder (zukünftig) grafische Notationen lassen sich ohne konzeptionellen Bruch mit textuellen Notationen integrieren. Siehe hierzu auch die Tabelle in Abbildung 1.

Erweiterungen

Vorkonfigurierte Erweiterungen

Die zentrale Idee von mbeddr ist, dass sich Anwender eigene, auf ihre Domäne zugeschnittene Erweiterungen bauen können. Nach einer Einarbeitung in MPS lassen sich solche Erweiterungen mit wenig Aufwand entwickeln. Nichtsdestoweniger umfasst mbeddr eine Reihe Erweiterungen, die allgemein genug gehalten sind, dass sie sich in vielen Embedded-Projekten sinnvoll einsetzen lassen. Einige seien im Folgenden beschrieben.

Unit-Testing und Error Reporting

Die technisch gesehen einfachste Erweiterung unterstützt Unit-Tests. Testfälle lassen sich direkt auf oberster Ebene in Modulen implementieren. Innerhalb von Testfällen stehen assert- und failStatements zur Verfügung (siehe Abb. 2).

Logging

Das Logging von Nachrichten ist in eingebetteten Systemen nicht einfach, da abhängig vom Zielgerät gegebenenfalls keine Konsole zur Verfügung steht, sondern die Nachrichten in einen Fehlerspeicher abzulegen sind. Außerdem sollten deaktivierte Log-Nachrichten nicht zu Laufzeit-Overhead führen. mbeddr kommt mit Sprachunterstützung für Logging, die sich durch modifizierbare Generatoren auf unterschiedliche Ausgabeziele anpassen lässt.

Physikalische Einheiten

Die Verwendung physikalischer Einheiten als Teil von Typen und Literalen vermeidet eine ganze Klasse von Fehlern. Die mbeddr-Erweiterung dafür bettet physikalische Einheiten direkt in das C-Typsystem ein. Physikalische Einheiten lassen sich an Typen und Literale annotieren. Das entsprechend erweiterte Typsystem erkennt, wenn Äpfel und Birnen addiert werden, und geht außerdem korrekt mit den Exponenten der Einheiten bei Multiplikation und Division um (siehe das Beispiel mit Länge und Zeit) (Abb. 3).

Die Benutzer der Spracherweiterung können eigene abgeleitete Einheiten definieren. Mit der Spracherweiterung lassen sich weitere primitive Einheiten definieren, die nicht zwangsläufig etwas mit den vordefinierten SI-Einheiten zu tun haben müssen. Beispiele dafür sind Koordinatensysteme oder Währungen.

Programmmodularisierung

Schnittstellen und Komponenten sind das primäre Mittel zur Programmmodularisierung (nicht zu verwechseln mit Sprachmodularisierung). Eine Schnittstelle spezifiziert eine Menge von Operationen inklusive Parametern und Rückgabetypen. Zusätzlich können Operationen auch Vor- und Nachbedingungen spezifizieren und damit die Semantik der Schnittstelle definieren. Abbildung 4 zeigt ein Beispiel. mbeddr unterstützt außerdem Protokollzustandsmaschinen zur Beschreibung der gültigen Aufrufreihenfolge von Operationen.

Komponenten können Schnittstellen anbieten oder benötigen. Die Implementierung der Operationen angebotener Schnittstellen geschieht mit normalem C-Code. Dabei ist sichergestellt, dass alle Komponenten, die eine bestimmte Schnittstelle anbieten, auch die Vor- und Nachbedingungen sowie die Protokollzustandsmaschine zur Laufzeit überprüfen. Benötigte Schnittstellen realisieren letztlich Dependency Injection. Bei der Instanziierung muss eine Komponente Zugriff auf andere Instanzen bekommen, die die von ihr benötigten Schnittstellen enthalten. Abbildung 5 zeigt das Beispiel einer Komponente.

Man beachte, dass eine Komponente nur die Schnittstellen angibt, die sie benötigt, nicht aber die implementierende Komponente. Das System unterstützt demnach Polymorphismus bei der Schnittstellenimplementierung. Da das einen gewissen Laufzeit-Overhead zur Folge hat (Indirektion via Funktionszeiger), lässt sich die Unterstützung für den Polymorphismus auch abschalten. In dem Fall verliert man Flexibilität, gewinnt aber etwas Performance.

Die Komponentenerweiterung unterstützt darüber hinaus Stubs und Mocks, um Komponenten effektiv testen zu können.

Zustandsmaschinen und Model Checking

Zustandsbasiertes Verhalten ist in eingebetteten Systemen allgegenwärtig. mbeddr unterstützt es durch direkt in C eingebettete Zustandsmaschinen (siehe Abb. 6).

Derzeit sind die Zustandsmaschinen noch textuell, bis Mitte 2013 wird eine zusätzliche grafische Syntax dafür zur Verfügung stehen. Man beachte, dass die Guards in den Zustandsmaschinen normale C-Ausdrücke sind, auch eine Form von Sprachwiederverwendung.

Ein großer Vorteil von Zustandsmaschinen liegt in ihrer guten Verifizierbarkeit. Mit Model Checking lassen sich alle Eigenschaften von Zustandsmaschinen zeigen. Für die, die als verifiable markiert sind, überprüft mbeddr automatisch eine Reihe von Eigenschaften (beispielsweise die Tatsache, dass alle Zustände irgendwann auch erreicht werden und dass es keine nichtdeterministischen Transitionen gibt). Benutzer können außerdem eigene zu beweisende Eigenschaften festlegen. Model Checking in mbeddr ist mit dem Werkzeug NuSMV implementiert. Die hier beschriebenen Verifikationsmechanismen sind derzeit noch nicht im Rahmen des Open-Source-Projekts verfügbar, werden aber im Laufe des dritten Quartals 2012 veröffentlicht.

Anforderungsverfolgung

mbeddr unterstützt das Erfassen von Anforderungen. Eine Anforderung hat eine eindeutige ID, eine textuelle Beschreibung und Beziehungen zu anderen Anforderungen. Die Art der Anforderung definiert, welche zusätzlichen formalen Spezifikationen sie aufweisen muss. Beispielsweise ließe sich eine Anforderung als Berechnungsvorschrift markieren, was dazu führen würde, dass die Formel zur Beschreibung der Berechnung zu erfassen wäre. Die unbegrenzte Sprachmodularisierung und Komposition von MPS erlaubt es, beliebige zusätzliche DSLs in die Sprache zur Anforderungserfassung zu integrieren. Ein Beispiel wäre eine DSL zur Beschreibung der oben genannten Berechnungsvorschriften.

Neben dem Erfassen von Anforderungen unterstützt mbeddr deren Nachverfolgbarkeit. Beliebige Programmelemente (ausgedrückt in beliebigen Sprachen) können sogenannte Trace-Links besitzen. Diese sind letztlich typisierte Zeiger auf ein oder mehrere Anforderungen (die grünen Annotationen in Abb. 7). Hier nutzt MPS wieder die Vorteile des projizierenden Editors: Die durch Trace-Links zu annotierende Sprache muss nicht geändert werden, um solche Annotationen anbringen zu können. Außerdem lässt sich die Anzeige der Links ein- und ausschalten.

Produktlinienvariabilität

Die zentrale Herausforderung bei Softwareproduktlinien besteht in der skalierbaren Umsetzung der Variabilität der einzelnen Produkte innerhalb der Produktlinie. In C erledigt das typischerweise der Präprozessor, der einzelne Textabschnitte entfernt, wenn das betreffende Symbol nicht definiert ist. In mbeddr steht ein anderer Ansatz zur Verfügung, der nicht auf Text-, sondern auf Strukturebene arbeitet. Beliebige Programmelemente (ausgedrückt in beliebigen Sprachen) lassen sich mit sogenannten Presence Conditions versehen. Das sind boolesche Ausdrücke über Konfigurationsschalter (tatsächlich sind das Features in Featuremodellen). Falls während der Generierung ein solcher Ausdruck zu false evaluiert, werden das betreffende Element und sowie alle Kinder aus dem Programm entfernt und damit nicht kompiliert. Das Zurechtschneiden des Programmbaums lässt sich nicht nur im Rahmen der Generierung durchführen, sondern auch im Editor selbst: Der Entwickler kann Programme in jeder beliebigen Variante betrachten und bearbeiten.

Status quo

Weitere Features

Die Spracherweiterung steht im Zentrum von mbeddr. Nichtsdestotrotz sind auch andere Features relevant:

• Header-Import: Damit Entwickler mbeddr in realistischen Umfeldern verwenden können, müssen sie auf existierenden Code zugreifen können. Das bedeutet insbesondere, Bibliotheken einzubinden. In C heißt das, dass textuelle Header-Dateien zu importieren sind, um die darin definierten Programmelemente aus dem mbeddr-C-Code ansprechen zu können. Der hierfür notwendige Mechanismus ist in mbeddr vorhanden und wird derzeit in ersten Projekten praktisch eingesetzt.
• Debugger: Erweiterbare Sprachen wie mbeddr C sind ein guter Kompromiss zwischen Programmierung (im Sinne von Verwendung von Programmiersprachen) und Modellierung (im Sinne des Einsatzes von DSLs), denn die Programmiersprache lässt sich schrittweise in Richtung der Domäne erweitern. Um das Potenzial vollständig auszuschöpfen, muss der Debugger über die Erweiterungen Bescheid wissen. Konkret bedeutet das, dass ein C-Programm mit domänenspezifischen Erweiterungen auf der Abstraktionsebene der Erweiterungen zu debuggen ist. Der mbeddr-Debugger ist im Rahmen der Definition der Spracherweiterungen entsprechend erweiterbar.
• Formale Verifikation: mbeddr unterstützt die Verifikation von Zustandsmaschinen. Daran lässt sich erkennen, dass Verifikation einfacher wird, wenn das Programm mit den richtigen Abstraktionen ausgedrückt wird. Für Model Checking eignen sich zustandsbasierte Abstraktionen. Da man mit mbeddr beliebige Abstraktionen in den C-Code integrieren kann, ergeben sich noch andere Optionen für die Integration formaler Verifikationsmethoden. Beispielsweise verwendet mbeddr SAT Solving, um die Konsistenz und Vollständigkeit von Entscheidungstabellen und Produktlinienkonfigurationen zu überprüfen. Des Weiteren existiert ein Prototyp zur Integration mit Frama-C. Damit lassen sich verschiedene relevante Eigenschaften von C-Code verifizieren.

Aktueller Stand

mbeddr wird im Rahmen eines BMBF-geförderten KMU-Innovativ-Projekts entwickelt, unter Beteiligung von itemis, ForTISS und Sick. Der Großteil von mbeddr ist Open Source. Die noch verbliebenen Anteile werden voraussichtlich noch 2012 veröffentlicht. Es kommt die Eclipse Public Licence zum Einsatz, die eine gewerbliche Verwendung des Codes erlaubt.

Derzeit werden erste ernsthafte Projekte mit mbeddr umgesetzt. Weitere Informationen zu mbeddr, inklusive detaillierten technischen Dokumentationen und Beutzerhandbücher sowie die Download-Packages und das Repository finden sich unter mbeddr.com sowie dem von dort verlinkten GitHub-Repository.

Markus Völter
arbeitet als freiberuflicher Berater und Coach für die itemis AG in Stuttgart. Seine Schwerpunkte liegen auf Architektur, modellgetriebener Softwareentwicklung und domänenspezifischen Sprachen sowie Produktlinien-Engineering.

Bernd Kolb
arbeitet als Architecture & Technology Manager bei der itemis AG in Stuttgart. Seine Schwerpunkte liegen auf der modellgetriebenen Software- und Tool-Entwicklung in verschiedenen Anwendungsbereichen von Automotive bis zu Cloud-Systemen. (ane)