Contract-based Modelling and Design

Contract-based Modelling and Design

Softwaremodellierung als vernetzte, zertifizierte Komponenten

Contract-based Modelling and Design

Um die Komplexität aktueller Softwaresysteme zu beherrschen, werden Softwarearchitekturen häufig um Produktfunktionen ergänzt.

Projektbeschreibung

Solche Produktfunktionen werden zum Beispiel durch Zustandsmaschinen oder MatLab/SimuLink-Modelle implementiert. Dieser Ansatz zeichnet sich aus durch die einfache Implementierbarkeit von auch komplizierten, nichtlinearen Funktionen mit zahlreichen Betriebsmodi sowie durch große Flexibilität und leichte Modifizierbarkeit. Sein Nachteil ist jedoch die unvorstellbar große Zahl von unbekannten und unerwünschten Zuständen, die solche Zustandsmaschinen oder MatLab/SimuLink-Modelle einnehmen können. Einer MIT-Studie von 2007 zufolge können sogar Systeme mit relativ einfachen Funktionen wie das Kollisionswarnsystem TCAS bis zu 1040 Zustände einnehmen. Moderne Motorsteuergeräte bringen es problemlos sogar auf über 10120 Zustände.

Die Contract-Based-Design-Methode (CBD) stellt eine Lösung für diese Problematik dar. Im Gegensatz zur analytischen modellbasierten Entwicklung ist CBD konstruktiv, d.h. ein System ist aus Komponenten mit Schnittstellen aufgebaut, die Ein- und Ausgangsgrößen haben. Sogenannte Contracts schränken die Beziehungen zwischen Ein- und Ausgangsgrößen ein und sorgen somit dafür, dass die Komponenten korrekt miteinander kommunizieren. Zudem wird auf diese Weise auch die Zahl unerwünschter Zustände im Gesamtsystem begrenzt. CBD garantiert also, dass die Eigenschaften und Zustände der beteiligten Komponenten eines Systems nicht ausufern und somit beherrschbar bleiben.

Forschungsbeitrag

eTrice ist ein ausgereiftes, modellbasiertes Open-Source-Software-Engineering-Tool. Es basiert auf der ROOM-Methodologie und wurde von der Protos GmbH, einem Projektpartner, konzipiert. Aktuell wird eTrice in der Industrie für die Entwicklung von Lösungen etwa in den Bereichen Gesundheit, Schwermaschinen und Automotive verwendet und bietet integrierte Mechanismen für die Laufzeitverifizierung. Auf Anregung der Entwickler von eTrice hat das Team von fortiss zudem Model Checking in seine Werkzeugkette integriert.

Die Forschungsergebnisse sind für Protos als Unternehmen sehr vielversprechend. Wir konnten anhand eines konkreten Beispiels zeigen, dass wichtige Eigenschaften eines Systems mit eTrice-Spezifikationen getestet werden können, ohne in irgendeiner Weise in die vorliegende Spezifikationssprache einzugreifen. Basierend auf unseren Arbeiten können nun Eigenschaften, die nicht per Laufzeitverifizierung kontrolliert werden konnten, über eTrice-Spezifikationen geprüft werden. Außerdem sorgt Model Checking für große Effizienz bei der Prüfung, und dies schon während der Entwicklungsphase und unter Berücksichtigung von in der Praxis eventuell sehr selten auftretenden Corner Cases. Aufgrund unserer Erfahrungen sind wir der Auffassung, dass der CBD-Ansatz mit vertretbarem Aufwand auf andere Entwicklungsumgebungen ausgeweitet werden kann.

Dr. Sebastian Voss

Ihr Ansprechpartner

Dr. Sebastian Voss

+49 89 3603522 33
voss@fortiss.org

Projektpartner

itemis AG - Model Based Software DevelopmentProtos GmbHSQMi GmbHUniversität Augsburg