Spracherweiterungen und Verifikation: C Entwicklung für das 21. Jahrhundert mit mbeddr
Markus Völter, Bernd Kolb, Dr. Daniel Ratiu
Zusammenfassung
Was wäre, wenn sich Sprachen genauso leicht erweitern ließen wie Programme? Entwickler könnten sich dann domänenspezifische Erweiterungen für Programmiersprachen bauen, was zu höherer Produktivität (durch weniger Code) und besserer Softwarequalität (durch bessere Analysierbarkeit) führt.
In diesem Tutorial demonstrieren wir diesen Ansatz basierend auf mbeddr, einer erweiterbaren Version von C die auf der JetBrains MPS Language Workbench beruht. mbeddr C kommt bereits mit einer Reihe von modularen Erweiterungen, darunter Komponenten, Zustandsmaschinen und Datentypen mit Maßeinheiten. Formale Verifikation mittels Model Checking und SMT Solving wird direkt unterstützt.
Im Tutorial erläutern wir die Idee und die Konzepte hinter inkrementeller Spracherweiterung und zeigen diese am Beispiel eingebetteter Softwareentwicklung mit mbeddr. Des Weiteren erstellen wir eine einfache Erweiterung um das Vorgehen zu illustrieren. Sowohl mbeddr als auch die Basistechnologie JetBrains MPS sind Open Source Software, sodass die Teilnehmer selbst mit dem System experimentieren können.
Ziele
- Warum ist inkrementelle Spracherweiterung sinnvoll?
- Wieviel Aufwand ist es, die mit geeigneten Werkzeugen zu erreichen?
- Wie kann man formale Methoden leichtgewichtiger einsetzen?
Thema
mbeddr ist ein Open Source Projekt welches die Entwicklung eines erweiterbaren C inklusive zugehöriger IDE zum Ziel hat. Basierend auf JetBrains MPS, einer Language Workbench, kann die Programmiersprache C um domänenspezifische Sprachkonstrukte erweitert werden. Existierende Erweiterungen umfassen Interfaces und Komponenten, Zustandsmaschinen, Datentypen mit Maßeinheiten sowie die Unterstützung für Requirements Tracing und Produktlinienvariabilität. Nutzer können jederzeit eigene, modulare Erweiterungen entwickeln und nutzen. Des Weiteren sind alle Spracherweiterungen auf der Ebene der neuen Abstraktion debugbar.
Programme die mittels adäquater Abstraktionen beschrieben sind lassen sich leichter analysieren. Durch die Nutzung adäquater Konstrukte sind viele Fehler vermeidbar (Stichwort: correct-by-construction, constructive quality assurance). Aus diesem Grund integriert mbeddr formale Verifikationsmethoden, darunter Model Checking, SMT Solvers sowie deductive deduktive Verifikation mit Frama-C.
Durch die Kombination von Spracherweiterung, fortgeschrittene Typenüberprüfungen, Erweiterungen des Typsystems mit Qualifiers, Definition von Constraints und formalen Methoden lässt sich die Qualität und Zuverlässigkeit von Software für eingebettete Systeme sowie die Entwicklerproduktivität erhöhen.
Weitere Informationen zu mbeddr finden sich unter http://mbeddr.com sowie in folgendem Paper.
