Startseite

 Termine

 Calls / Einreichungen

 Programm

 Keynotes

 Rahmenprogramm

 Anmeldung

 Hotels

 Tagungsort

 Anreise

 Geschichte

 Programmkomitee

 Kontakt

Veranstaltungen


 SE2013 - Startseite

 SEE

 SEUH

 Doktorandensymposium

 Studierendentag

 Workshops / Tutorien

Sponsoren

Platin




Gold






















Silber






Bronze








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


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.