ESE Fachwissen
Der richtige Einstieg in modellbasiertes Software Engineering?
Autor: Georg Rößler, peiker acustic GmbH & Co. KG, Valeo peiker Telematics
Beitrag - Embedded Software Engineering Kongress 2016
Die Vorteile von modellbasierter Softwareentwicklung (MBSE – Model Based Software Engineering) sind vielfach beschrieben worden. Dennoch ist die Methode weniger verbreitet, als dies zu erwarten wäre, weil beim Einstieg einige Hürden zu überwinden sind. Oft entstehen neue Produkte auf der Basis eines vorhandenen Systems mit konventionell entwickelter Software. Außerdem erwartet der Auftraggeber häufig, dass frühzeitig einige Funktionen demonstriert und im Zuge der Entwicklung erweitert werden.
Dieser Beitrag zeigt am Beispiel eines Telematik-Steuergeräts für den Notruf im Auto, wie sich die Schwierigkeiten überwinden lassen. Neue Funktionen werden modellbasiert entwickelt, indem aus den Zustandsautomaten des UML-Modells Code generiert wird. Die Vorgehensweise ist darauf ausgelegt, dass die neuen Funktionen sich leicht in das bestehende System integrieren lassen. Im zweiten Teil beschreibt der Artikel, wie Zustandsautomaten mit dem Tool Spin durch Simulation und durch formale Verifikation auf Korrektheit überprüft werden können.
Steuergerät für ERA-GLONASS-Notruf
Die Aufgabe im Projekt bestand darin, ein Steuergerät für den Notruf im Auto entsprechend den ERA-GLONASS-Standards für den russischen Markt zu entwickeln. ERA-GLONASS basiert auf dem standardisierten Notruf in der EU (EU eCall), der ab dem Frühjahr 2018 in allen in der EU neu zugelassenen Automodellen vorgeschrieben ist. ERA-GLONASS ist zum EU eCall kompatibel, trifft jedoch eine ganze Reihe weiterer Festlegungen, die in den EU-Standards den jeweiligen Herstellern der Autos oder der Telematik-Steuergeräte überlassen werden. Die Abbildung 1 (siehe PDF) zeigt das ERA-GLONASS-Steuergerät mit seinen externen Schnittstellen und angeschlossenen Einheiten.
Das Steuergerät wurde auf der Basis eines UMTS-NAD (NAD – Network Access Device) realisiert, das von einem anderen Steuergerät übernommen werden konnte. Das NAD stellte schon alle Basisfunktionen wie Telefonie, SMS und Datenverbindungen zur Verfügung, und es war eine prototypische Realisierung des EU eCalls vorhanden. Für die Ansteuerung der Hardware-Schnittstellen wurde eine neue Baugruppe mit einem eigenen Mikrocontroller realisiert, der mit dem Applikationscontroller auf dem NAD über eine serielle Schnittstelle und einige dedizierte Hardwareleitungen kommuniziert.
Codegenerierung aus dem Zustandsautomaten
Die Option, den Notruf entsprechend den ERA-GLONASS-Standards auf der Basis des EU eCall-Prototyps zu entwickeln, wurde rasch verworfen, weil als Endzustand eine schlecht strukturierte Implementierung mit vielen "Erkern" zu erwarten war. Stattdessen wurde die neue Funktion mit UML modelliert, und aus dem Zustandsautomaten im Modell wurde auch direkt der Code für das Verhalten generiert.
Damit die Codegenerierung sinnvoll einsetzbar ist, müssen zwei Anforderungen erfüllt sein:
- Der generierte Code muss leicht in ein vorhandenes System integrierbar sein. Häufig resultiert daraus die Anforderung, dass der generierte Code ohne eigene Laufzeitumgebung auskommen muss, weil eine ungewöhnliche Zielumgebung vorgegeben ist.
- Bei der Weiterentwicklung des Zustandsautomaten muss der generierte Code sehr leicht integrierbar sein. Andernfalls ist weder eine iterative Entwicklung möglich, noch kann man rasch auf geänderter Anforderungen reagieren oder Fehler sicher korrigieren.
Als Codegenerator wurde eine vorhandene Eigenentwicklung verwendet, die aus Zustandsautomaten Java-Code erzeugt. Die vorhandenen Funktionen für den Import aus UML und die internen Repräsentationen konnten unverändert bleiben. Nur die Erzeugung von C-Code wurde neu implementiert. Die Anforderung dabei war, dass Dateien entweder vollständig generiert werden, oder sie werden rein manuell erstellt.
Das Konzept für die Codegenerierung ist inspiriert von einem Lastgenerator für Telefonsysteme [1], der nach dem Start des Programms SDL-Modelle einliest und das spezifizierte Verhalten realisiert. Die Lösung beruht darauf, dass die SDL-Modelle in Datenstrukturen abgebildet werden, die von einer allgemeinen Ablaufsteuerung interpretiert werden. Anstatt die Datenstrukturen für den spezifischen Zustandsautomaten zur Laufzeit anzulegen, werden sie durch den Codegenerator statisch erzeugt.
Mit dem einfachen Zustandsautomaten in Abbildung 2 (siehe PDF) konnte die Grundfunktion für den Notruf früh realisiert werden. Dieser Automat mit nur 6 Zuständen verarbeitet 14 verschiedene Trigger in 17 Zustandsübergängen.
Im Lauf der Entwicklung wurden nacheinander Funktionen hinzugefügt und verfeinert. Mit dem in ERA-GLONASS geforderten Testruf kam ein weiterer Zustand dazu, und der Automat verarbeitete 22 Trigger in 34 Übergängen. Für die komplette Funktionalität wurden vor allem komplexere Fehlerbehandlungen nach Verbindungsabbrüchen oder fehlgeschlagenen Versuchen ergänzt. Der Automat wuchs dadurch auf 9 Zustände und 49 Übergänge an, die durch 25 verschiedene Trigger ausgelöst werden.
Die Steuerung der Betriebszustände wurde für das ERA-GLONASS-Steuergerät ebenfalls neu implementiert sowie das Verhalten auf dem NAD in einem zweiten Automaten modelliert und daraus direkt der Code generiert.
Simulation von Zustandsautomaten in UML
Die Steuerung der Betriebszustände ist eine kritische Funktion in jedem Notruf-Steuergerät. Einerseits muss das Steuergerät in einen Modus mit minimaler Stromaufnahme wechseln, wenn das Auto in Ruhe ist. Andererseits muss es im Falle eines Notrufs unbedingt aktiv bleiben, unabhängig vom übrigen Zustand des Fahrzeugs. Darüber hinaus muss das Notruf-Steuergerät für einige Zeit im Netz eingebucht bleiben, damit es von der Notrufzentrale für Rückrufe und für Aufträge per SMS erreichbar bleibt.
Weil die Trigger für Zustandswechsel in beliebiger Reihenfolge eintreffen können, müssen die korrekte Funktion des Automaten unter allen Umständen sichergestellt werden.
Als erste Möglichkeit wurde dafür die Simulation des Zustandsautomaten mit einem UML-Tool erprobt. Für die Umgebung des Zustandsautomaten auf dem NAD wurden weitere Automaten entworfen, welche Trigger für den zu testenden Automaten erzeugen. Für die Trigger vom Auto wurde ein Zustandsautomat entworfen, der die Klemmensignale erzeugt. Diese werden von einem zweiten Automaten auf der MCU verarbeitet und relevante Änderungen in Nachrichten an das NAD umgesetzt, die dann vom Zustandsautomaten für die Betriebszustände verarbeitet werden.
In einem Modell mit diesen drei Zustandsautomaten konnten einzelne Abläufe manuell durchgespielt werden. Beim Test mit dem automatischen Modus stellte sich jedoch heraus, dass bestimmte Abläufe nie vorkamen, obwohl sie möglich waren. Die Ursache für dieses Verhalten ist vermutlich, dass die Anzahl der Zustandsübergänge für die vernachlässigten Übergänge wesentlich größer war als für diejenigen, die beim automatischen Ablauf tatsächlich vorkamen.
Für die Automaten der Umgebung ließ sich zufälliges Verhalten noch durch explizite Modellierung von zufälligen Verzweigungen erzwingen. Für das Zusammenspiel zwischen dem zu überprüfenden Automaten und der Umgebung war dieser Ansatz jedoch nicht ausreichend. Manche Abläufe traten bei der automatischen Simulation nie auf, obwohl sie im Modell vorgesehen und möglich waren.
Übertragung der Zustandsautomaten nach Spin
Für die weitere Überprüfung von Zustandsautomaten wurde in der Folge das Werkzeug Spin [2], [3] verwendet. Dadurch musste der Zustandsautomat NAD Lifecycle für die Betriebszustände auf dem NAD sowie die umgebenden Automaten in der Sprache Promela beschrieben werden, die Spin verwendet.
Das gesamte Modell besteht aus sechs Prozessen, die miteinander interagieren. Als Interaktionsmechanismen sind mit Spin Rendezvous für den synchronen Austausch von Meldungen und Kanäle mit Meldungspuffern für die asynchrone Kommunikation möglich. Außerdem können Prozesse über Variablen interagieren, die sie gemeinsam nutzen.
Abbildung 3 (siehe PDF) zeigt ein Modell für die Untersuchung der Spin. Dünne Linien zeigen synchrone Interaktion an, dicke Linien asynchrone Kommunikation über Kanäle mit Meldungspuffern.
Die Syntax von Promela ähnelt gängigen Programmiersprachen, jedoch mit dem wichtigen Unterschied, dass nicht-deterministisches Verhalten möglich ist. Der folgende Ausschnit aus dem Prozess mculifecycle stellt dar, dass das Steuergerät durch das Einschalten der Zündung oder durch den Notrufknopf für den manuellen Notruf gestartet werden kann.
ONLY_MANUAL:
printf( " MCU: ERA_ONLY_MANUAL " );
/* keine Meldungen vom letzten Zyklus im Puffer */
assert( len(rpcNadMcu) == 0 );
do
:: atomic
{
( gIgnitionOn == true ) ->
gIgnEnable = 3;
pMcuNadOn!NadPwrOn;
}
/* Kommunikation über serielle Schnittstelle starten */
mcuOpenAspConnection();
rpcMcuNad!sysmode, modeOn;
goto ERA_ON;
:: pEbttnMcu ? param ->
assert( param == true );
pMcuNadOn!NadPwrOn;
mcuOpenAspConnection();
rpcMcuNad!trgevt, EcallButton;
rpcMcuNad!sysmode, modeEcall;
goto ECALL;
:: ( gIgnEnable == 0 ) ->
gIgnEnable = 1;
od
Der Prozess bietet in diesem Zustand beide Möglichkeiten für den Start des Systems an (gIgnitionOn, pEbttnMcu). Wenn die Gegenseite peripheralproc nur eine anbietet, wird der entsprechende Zweig ausgewählt. Sofern peripheralproc jedoch beide Möglichkeiten anbietet, wird bei der Simulation zufällig eine der Optionen ausgewählt. Bei der Verifikation werden beide Möglichkeiten im Zustandsraum ausgewertet.
Während es in der Realität quasi unmöglich ist, gleichzeitig die Zündung einzuschalten und den Notrufknopf zu drücken, ist das im Modell in Spin ohne Weiteres vorgesehen. Es kommt bei Spin nicht auf die Zeit an, die einzelne Schritte benötigen, sondern nur auf die Reihenfolge, in der sie auftreten. Dabei werden alle Abläufe akzeptiert, die im Modell prinzipiell möglich ist. Im Beispiel kann also peripheralproc zuerst die Zündung einschalten, dann den Notrufknopf drücken und schließlich in mculifecycle auf eines der beiden Angebote eingehen.
Als dritte Möglichkeit im gezeigten Ausschnitt wird der Kredit für einen Zündungswechsel (gIgnEnable) erneuert. Der Mechanismus mit dem Kredit wurde eingeführt, damit bei Verklemmungen (Deadlocks) im restlichen System die Simulation auch wirklich stoppt; andernfalls wird die Zündung in einer unproduktiven Schleife noch beliebig oft umgeschaltet.
Simulatin und Verifikation mit Spin
Das Modell wurde in einem ersten Schritt ohne den Notruf erstellt (ohne ecallmanager und ohne nadrpcrec). Für den Automaten nadlifecycle wurde die Übereinstimmung mit dem UML-Modell, das für die Codegenerierung verwendet wurde, durch Review geprüft. Der Automat mculifecycle entstand nach der Spezifikation, die auch für die Implementierung verwendet wurde.
Bei den ersten Simulationen traten verschiedene Probleme auf. Diese werden durch Verklemmungen angezeigt oder durch Verletzung von Assertions, die explizit im Modell eingefügt wurden, um unerwünschtes Verhalten aufzudecken. Die Mehrzahl der Probleme ging nicht auf Fehler in den Automaten zurück, sondern auf ungeeignete oder unvollständige Repräsentationen für Spin. In dieser Phase wurden auch unterschiedliche Formen für die Modellierung des Timers für die Nachlaufzeit nach dem Ausschalten der Zündung erprobt, bis dann die Form mit zwei Flags (TimerActive; Timeout) als geeignet gefunden wurde. Diese Modellierung kommt der Implementierung nahe, die für den Timer einen Zähler führt, der in einem festen Takt dekrementiert wird.
Die Simulation mit Spin läuft sehr effizient ab, so dass man auf einem normalen Notebook in einer virtuellen Maschine mit Linux Simulationsläufe mit hundert Millionen Schritten in wenigen Minuten ausführen kann. Nachdem diese langen Simulationen fehlerfrei liefen, wurde Spin im Verifikationsmodus verwendet. Dabei wird der komplette Zustandsraum untersucht, wobei Spin das berüchtigte Problem der Zustandsraumexplosion durch verschiedene Methoden löst oder vermeidet.
Bei der Verifikation können neue Probleme aufgedeckt werden, weil dabei der Zustandsraum auch auf Schleifen ohne Fortschritt hin analysiert wird. Auf diese Weise werden Fehlerfälle aufgedeckt wie die Situation, dass nur noch die Zündung umgeschaltet wird.
Nachdem das einfache Modell erfolgreich simuliert und verifiziert war, wurden die beiden Prozesse für den Notruf hinzugefügt. Die Meldungskommunikation entspricht damit auch dem realen System, in dem Meldungen von der seriellen Leitung anhand ihres Typs an die richtigen Empfänger verteilt werden.
Zusammenfassung und Empfehlungen
In dem Artikel wurde die Entwicklung eines ERA-GLONASS-Steuergeräts für den Notruf im Auto vorgestellt, bei dem für wichtige neue Funktionen modellbasiertes Software Engineering eingesetzt wurde. Das Verhalten für den Notruf und für die Steuerung der Betriebszustände wurde durch Zustandsautomaten modelliert und daraus der Code für die Abläufe generiert. Entscheidend für den Erfolg war, dass die Automaten während der Entwicklung schrittweise erweitert und korrigiert werden konnten, weil sich der neu generierte Code mit minimalem Aufwand integrieren ließ.
Die resultierende Implementierung funktionierte von vornherein einwandfrei und war auch bei vielfachen Wiederholungen im Systemtest absolut stabil und zuverlässig. Da Modell und Code durch Konstruktion übereinstimmten, ließen sich Fragen zum Verhalten direkt aus dem Modell beantworten.
Das Beispiel zeigt, dass es auch bei Entwicklungen auf der Basis eines vorhandenen Systems möglich und lohnend ist, neue Teile modellbasiert zu entwickeln. Für die Umsetzung ist folgende Vorgehensweise zu empfehlen:
- Neue Funktionen identifizieren, die für modellbasiertes Software Engineering in Frage kommen
- Codegenerator passend zur Aufgabe und zur Zielumgebung auswählen. Wichtig ist, dass neu generierter Code leicht integrierbar ist.
- Ausgewählte neue Funktionen von Anfang an modellbasiert entwickeln
- Mit Basisfunktion beginnen, um die Vorgehensweise und die Werkzeuge zu erproben
- Sukzessive weitere Funktionalität ergänzen
Neben dem überschaubaren Risiko beim Übergang zu modellbasierter Entwicklung hat diese Vorgehensweise den Vorteil, dass die Entwickler langsam an die neue Entwicklungsmethodik herangeführt werden und so eventuelle Vorbehalte leichter überwunden werden können.
Im zweiten Teil wurde die Simulation und formale Verifikation des Zustandsautomaten für die Steuerung der Betriebszustände mit Spin vorgestellt und dabei auf einige Besonderheiten der Methode eingegangen. Die Verhaltensbeschreibungen in Spin sind durch die Abstraktion einerseits recht kompakt und andererseits nahe genug an der Implementierung, um für diese gültige Aussagen zu treffen.
Mit Spin ist ein Werkzeug verfügbar, das sich für die formale Verifikation von realen Systemen eignet und nicht nur für kleine Beispiele. Wer also bei der Überprüfung von Zustandsautomaten über Reviews und ausgefeilte Tests hinausgehen will, kann mit Spin das Verhalten durch Simulation und durch formale Verifikation überprüfen und dabei Verklemmungen, Zyklen ohne Fortschritt und unerwünschtes Verhalten schon im Modell aufdecken und beheben.
Referenzen
[1] T. Steinert, G. Rößler, "Generation of realistic signalling traffic in an ISDN load test system using SDL User Models", Proceedings of FORTE/PSTV 2000, Pisa.
[2] Spin Webseite. http://spinroot.com/
[3] M. Ben-Ari, "A Primer on Model Checking", ACM Inroads 2010 March, Vol. 1, No. 1. Verfügbar unter
http://spinroot.com/spin/Doc/p40-ben-ari.pdf
Modellierung - MicroConsult Trainings & Coachings
Wollen Sie sich auf den aktuellen Stand der Technik bringen?
Dann informieren Sie sich hier zu Schulungen/ Seminaren/ Trainings/ Workshops und individuellen Coachings von MircoConsult zum Thema Modellierung /Embedded- und Echtzeit-Softwareentwicklung.
Training & Coaching zu den weiteren Themen unseren Portfolios finden Sie hier.
Modellierung - Fachwissen
Wertvolles Fachwissen zum Thema Modellierung /Embedded- und Echtzeit-Softwareentwicklung steht hier für Sie zum kostenfreien Download bereit.
Fachwissen zu weiteren Themen unseren Portfolios finden Sie hier.