Autor: Georg R\u00f6\u00dfler, peiker acustic GmbH & Co. KG, Valeo peiker Telematics<\/p>\n
Die Vorteile von modellbasierter Softwareentwicklung (MBSE \u2013 Model Based Software Engineering) sind vielfach beschrieben worden. Dennoch ist die Methode weniger verbreitet, als dies zu erwarten w\u00e4re, weil beim Einstieg einige H\u00fcrden zu \u00fcberwinden sind. Oft entstehen neue Produkte auf der Basis eines vorhandenen Systems mit konventionell entwickelter Software. Au\u00dferdem erwartet der Auftraggeber h\u00e4ufig, dass fr\u00fchzeitig einige Funktionen demonstriert und im Zuge der Entwicklung erweitert werden.<\/strong><\/p>\n Dieser Beitrag zeigt am Beispiel eines Telematik-Steuerger\u00e4ts f\u00fcr den Notruf im Auto, wie\u00a0 sich die Schwierigkeiten \u00fcberwinden 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\u00a0Spin<\/em>\u00a0durch Simulation und durch formale Verifikation auf Korrektheit \u00fcberpr\u00fcft werden k\u00f6nnen.<\/p>\n Die Aufgabe im Projekt bestand darin, ein Steuerger\u00e4t f\u00fcr den Notruf im Auto entsprechend den ERA-GLONASS-Standards f\u00fcr den russischen Markt zu entwickeln. ERA-GLONASS basiert auf dem standardisierten Notruf in der EU (EU eCall), der ab dem Fr\u00fchjahr 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\u00e4te \u00fcberlassen werden. Die Abbildung 1 (siehe\u00a0PDF<\/a>) zeigt das ERA-GLONASS-Steuerger\u00e4t mit seinen externen Schnittstellen und angeschlossenen Einheiten.<\/p>\n Das Steuerger\u00e4t wurde auf der Basis eines UMTS-NAD (NAD \u2013 Network Access Device) realisiert, das von einem anderen Steuerger\u00e4t \u00fcbernommen werden konnte. Das NAD stellte schon alle Basisfunktionen wie Telefonie, SMS und Datenverbindungen zur Verf\u00fcgung, und es war eine prototypische Realisierung des EU eCalls vorhanden. F\u00fcr die Ansteuerung der Hardware-Schnittstellen wurde eine neue Baugruppe mit einem eigenen Mikrocontroller realisiert, der mit dem Applikationscontroller auf dem NAD \u00fcber eine serielle Schnittstelle und einige dedizierte Hardwareleitungen kommuniziert.<\/p>\n 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\u00fcr das Verhalten generiert.<\/p>\n Damit die Codegenerierung sinnvoll einsetzbar ist, m\u00fcssen zwei Anforderungen erf\u00fcllt sein:<\/p>\n Als Codegenerator wurde eine vorhandene Eigenentwicklung verwendet, die aus Zustandsautomaten Java-Code erzeugt. Die vorhandenen Funktionen f\u00fcr den Import aus UML und die internen Repr\u00e4sentationen konnten unver\u00e4ndert bleiben. Nur die Erzeugung von C-Code wurde neu implementiert. Die Anforderung dabei war, dass Dateien entweder vollst\u00e4ndig generiert werden, oder sie werden rein manuell erstellt.<\/p>\n Das Konzept f\u00fcr die Codegenerierung ist inspiriert von einem Lastgenerator f\u00fcr Telefonsysteme [1], der nach dem Start des Programms SDL-Modelle einliest und das spezifizierte Verhalten realisiert. Die L\u00f6sung beruht darauf, dass die SDL-Modelle in Datenstrukturen abgebildet werden, die von einer allgemeinen Ablauf\u00adsteuerung interpretiert werden. Anstatt die Datenstrukturen f\u00fcr den spezifischen Zustandsautomaten zur Laufzeit anzulegen, werden sie durch den Codegenerator statisch erzeugt.<\/p>\n Mit dem einfachen Zustandsautomaten in Abbildung 2 (siehe\u00a0PDF<\/a>) konnte die Grundfunktion f\u00fcr den Notruf fr\u00fch realisiert werden. Dieser Automat mit nur 6 Zust\u00e4nden verarbeitet 14 verschiedene Trigger in 17 Zustands\u00fcberg\u00e4ngen.<\/p>\n Im Lauf der Entwicklung wurden nacheinander Funktionen hinzugef\u00fcgt und verfeinert. Mit dem in ERA-GLONASS geforderten Testruf kam ein weiterer Zustand dazu, und der Automat verarbeitete 22 Trigger in 34 \u00dcberg\u00e4ngen. F\u00fcr die komplette Funktionalit\u00e4t wurden vor allem komplexere Fehlerbehandlungen nach Verbindungsabbr\u00fcchen oder fehlgeschlagenen Versuchen erg\u00e4nzt. Der Automat wuchs dadurch auf 9 Zust\u00e4nde und 49 \u00dcberg\u00e4nge an, die durch 25 verschiedene Trigger ausgel\u00f6st werden.<\/p>\n Die Steuerung der Betriebszust\u00e4nde wurde f\u00fcr das ERA-GLONASS-Steuerger\u00e4t ebenfalls neu implementiert sowie das Verhalten auf dem NAD in einem zweiten Automaten modelliert und daraus direkt der Code generiert.<\/p>\n Die Steuerung der Betriebszust\u00e4nde ist eine kritische Funktion in jedem Notruf-Steuerger\u00e4t. Einerseits muss das Steuerger\u00e4t in einen Modus mit minimaler Stromaufnahme wechseln, wenn das Auto in Ruhe ist. Andererseits muss es im Falle eines Notrufs unbedingt aktiv bleiben, unabh\u00e4ngig vom \u00fcbrigen Zustand des Fahrzeugs. Dar\u00fcber hinaus muss das Notruf-Steuerger\u00e4t f\u00fcr einige Zeit im Netz eingebucht bleiben, damit es von der Notrufzentrale f\u00fcr R\u00fcckrufe und f\u00fcr Auftr\u00e4ge per SMS erreichbar bleibt.<\/p>\n Weil die Trigger f\u00fcr Zustandswechsel in beliebiger Reihenfolge eintreffen k\u00f6nnen, m\u00fcssen die korrekte Funktion des Automaten unter allen Umst\u00e4nden sichergestellt werden.<\/p>\n Als erste M\u00f6glichkeit wurde daf\u00fcr die Simulation des Zustandsautomaten mit einem UML-Tool erprobt. F\u00fcr die Umgebung des Zustandsautomaten auf dem NAD wurden weitere Automaten entworfen, welche Trigger f\u00fcr den zu testenden Automaten erzeugen. F\u00fcr die Trigger vom Auto wurde ein Zustandsautomat entworfen, der die Klemmensignale erzeugt. Diese werden von einem zweiten Automaten auf der MCU verarbeitet und relevante \u00c4nderungen in Nachrichten an das NAD umgesetzt, die dann vom Zustandsautomaten f\u00fcr die Betriebszust\u00e4nde verarbeitet werden.<\/p>\n In einem Modell mit diesen drei Zustandsautomaten konnten einzelne Abl\u00e4ufe manuell durchgespielt werden. Beim Test mit dem automatischen Modus stellte sich jedoch heraus, dass bestimmte Abl\u00e4ufe nie vorkamen, obwohl sie m\u00f6glich waren. Die Ursache f\u00fcr dieses Verhalten ist vermutlich, dass die Anzahl der Zustands\u00fcberg\u00e4nge f\u00fcr die vernachl\u00e4ssigten \u00dcberg\u00e4nge wesentlich gr\u00f6\u00dfer war als f\u00fcr diejenigen, die beim automatischen Ablauf tats\u00e4chlich vorkamen.<\/p>\n F\u00fcr die Automaten der Umgebung lie\u00df sich zuf\u00e4lliges Verhalten noch durch explizite Modellierung von zuf\u00e4lligen Verzweigungen erzwingen. F\u00fcr das Zusammenspiel zwischen dem zu \u00fcberpr\u00fcfenden Automaten und der Umgebung war dieser Ansatz jedoch nicht ausreichend. Manche Abl\u00e4ufe traten bei der automatischen Simulation nie auf, obwohl sie im Modell vorgesehen und m\u00f6glich waren.<\/p>\n F\u00fcr die weitere \u00dcberpr\u00fcfung von Zustandsautomaten wurde in der Folge das Werkzeug Spin [2], [3] verwendet. Dadurch musste der Zustandsautomat NAD Lifecycle f\u00fcr die Betriebszust\u00e4nde auf dem NAD sowie die umgebenden Automaten in der Sprache\u00a0Promela<\/em>\u00a0beschrieben werden, die Spin verwendet.<\/p>\n Das gesamte Modell besteht aus sechs Prozessen, die miteinander interagieren. Als Interaktionsmechanismen sind mit Spin Rendezvous f\u00fcr den synchronen Austausch von Meldungen und Kan\u00e4le mit Meldungspuffern f\u00fcr die asynchrone Kommunikation m\u00f6glich. Au\u00dferdem k\u00f6nnen Prozesse \u00fcber Variablen interagieren, die sie gemeinsam nutzen.<\/p>\n Abbildung 3 (siehe\u00a0PDF<\/a>) zeigt ein Modell f\u00fcr die Untersuchung der Spin. D\u00fcnne Linien zeigen synchrone Interaktion an, dicke Linien asynchrone Kommunikation \u00fcber Kan\u00e4le mit Meldungspuffern.<\/p>\n Die Syntax von Promela \u00e4hnelt g\u00e4ngigen Programmiersprachen, jedoch mit dem wichtigen Unterschied, dass nicht-deterministisches Verhalten m\u00f6glich ist. Der folgende Ausschnit aus dem Prozess\u00a0mculifecycle<\/em>\u00a0stellt dar, dass das Steuerger\u00e4t durch das Einschalten der Z\u00fcndung oder durch den Notrufknopf f\u00fcr den manuellen Notruf gestartet werden kann.<\/p>\n ONLY_MANUAL:<\/p>\n \u00a0\u00a0\u00a0 printf( “\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 MCU: ERA_ONLY_MANUAL “ );<\/p>\n \u00a0\u00a0\u00a0 \/* keine Meldungen vom letzten Zyklus im Puffer *\/<\/p>\n \u00a0\u00a0\u00a0 assert( len(rpcNadMcu) == 0 );<\/p>\n \u00a0\u00a0\u00a0 do<\/p>\n \u00a0\u00a0\u00a0 ::\u00a0 atomic<\/p>\n \u00a0\u00a0\u00a0 {<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 ( gIgnitionOn == true ) -><\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 gIgnEnable = 3;<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 pMcuNadOn!NadPwrOn;<\/p>\n \u00a0\u00a0\u00a0 }<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 \/* Kommunikation \u00fcber serielle Schnittstelle starten *\/<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 mcuOpenAspConnection();<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 rpcMcuNad!sysmode, modeOn;<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 goto ERA_ON;<\/p>\n \u00a0\u00a0\u00a0 ::\u00a0 pEbttnMcu ? param -><\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 assert( param == true );<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 pMcuNadOn!NadPwrOn;<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 mcuOpenAspConnection();<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 rpcMcuNad!trgevt, EcallButton;<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 rpcMcuNad!sysmode, modeEcall;<\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 goto ECALL;<\/p>\n \u00a0\u00a0\u00a0 ::\u00a0 ( gIgnEnable == 0 ) -><\/p>\n \u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 gIgnEnable = 1;<\/p>\n \u00a0\u00a0\u00a0 od<\/p>\n Der Prozess bietet in diesem Zustand beide M\u00f6glichkeiten f\u00fcr den Start des Systems an (gIgnitionOn, pEbttnMcu). Wenn die Gegenseite\u00a0peripheralproc<\/em><\/strong>\u00a0nur eine anbietet, wird der entsprechende Zweig ausgew\u00e4hlt. Sofern\u00a0peripheralproc<\/em><\/strong>\u00a0jedoch beide M\u00f6glichkeiten anbietet, wird bei der Simulation zuf\u00e4llig eine der Optionen ausgew\u00e4hlt. Bei der Verifikation werden beide M\u00f6glichkeiten im Zustandsraum ausgewertet.<\/p>\n W\u00e4hrend es in der Realit\u00e4t quasi unm\u00f6glich ist, gleichzeitig die Z\u00fcndung einzuschalten und den Notrufknopf zu dr\u00fccken, ist das im Modell in Spin ohne Weiteres vorgesehen. Es kommt bei Spin nicht auf die Zeit an, die einzelne Schritte ben\u00f6tigen, sondern nur auf die Reihenfolge, in der sie auftreten. Dabei werden alle Abl\u00e4ufe akzeptiert, die im Modell prinzipiell m\u00f6glich ist. Im Beispiel kann also\u00a0peripheralproc<\/em><\/strong>\u00a0zuerst die Z\u00fcndung einschalten, dann den Notrufknopf dr\u00fccken und schlie\u00dflich in\u00a0mculifecycle<\/em><\/strong>\u00a0auf eines der beiden Angebote eingehen.<\/p>\n Als dritte M\u00f6glichkeit im gezeigten Ausschnitt wird der Kredit f\u00fcr einen Z\u00fcndungswechsel (gIgnEnable) erneuert. Der Mechanismus mit dem Kredit wurde eingef\u00fchrt, damit bei Verklemmungen (Deadlocks) im restlichen System die Simulation auch wirklich stoppt; andernfalls wird die Z\u00fcndung in einer unproduktiven Schleife noch beliebig oft umgeschaltet.<\/p>\n Das Modell wurde in einem ersten Schritt ohne den Notruf erstellt (ohne\u00a0ecallmanager<\/em><\/strong>\u00a0und ohne\u00a0nadrpcrec<\/em><\/strong>). F\u00fcr den Automaten\u00a0nadlifecycle<\/em><\/strong>\u00a0wurde die \u00dcbereinstimmung mit dem UML-Modell, das f\u00fcr die Codegenerierung verwendet wurde, durch Review gepr\u00fcft. Der Automat\u00a0mculifecycle<\/em><\/strong>\u00a0entstand nach der Spezifikation, die auch f\u00fcr die Implementierung verwendet wurde.<\/p>\n Bei den ersten Simulationen traten verschiedene Probleme auf. Diese werden durch Verklemmungen angezeigt oder durch Verletzung von Assertions, die explizit im Modell eingef\u00fcgt wurden, um unerw\u00fcnschtes Verhalten aufzudecken. Die Mehrzahl der Probleme ging nicht auf Fehler in den Automaten zur\u00fcck, sondern auf ungeeignete oder unvollst\u00e4ndige Repr\u00e4sentationen f\u00fcr Spin. In dieser Phase wurden auch unterschiedliche Formen f\u00fcr die Modellierung des Timers f\u00fcr die Nachlaufzeit nach dem Ausschalten der Z\u00fcndung erprobt, bis dann die Form mit zwei Flags (TimerActive; Timeout) als geeignet gefunden wurde. Diese Modellierung kommt der Implementierung nahe, die f\u00fcr den Timer einen Z\u00e4hler f\u00fchrt, der in einem festen Takt dekrementiert wird.<\/p>\n Die Simulation mit Spin l\u00e4uft sehr effizient ab, so dass man auf einem normalen Notebook in einer virtuellen Maschine mit Linux Simulationsl\u00e4ufe mit hundert Millionen Schritten in wenigen Minuten ausf\u00fchren kann. Nachdem diese langen Simulationen fehlerfrei liefen, wurde Spin im Verifikationsmodus verwendet. Dabei wird der komplette Zustandsraum untersucht, wobei Spin das ber\u00fcchtigte Problem der Zustandsraumexplosion durch verschiedene Methoden l\u00f6st oder vermeidet.<\/p>\n Bei der Verifikation k\u00f6nnen neue Probleme aufgedeckt werden, weil dabei der Zustandsraum auch auf Schleifen ohne Fortschritt hin analysiert wird. Auf diese Weise werden Fehlerf\u00e4lle aufgedeckt wie die Situation, dass nur noch die Z\u00fcndung umgeschaltet wird.<\/p>\n Nachdem das einfache Modell erfolgreich simuliert und verifiziert war, wurden die beiden Prozesse f\u00fcr den Notruf hinzugef\u00fcgt. Die Meldungskommunikation entspricht damit auch dem realen System, in dem Meldungen von der seriellen Leitung anhand ihres Typs an die richtigen Empf\u00e4nger verteilt werden.<\/p>\n In dem Artikel wurde die Entwicklung eines ERA-GLONASS-Steuerger\u00e4ts f\u00fcr den Notruf im Auto vorgestellt, bei dem f\u00fcr wichtige neue Funktionen modellbasiertes Software Engineering eingesetzt wurde. Das Verhalten f\u00fcr den Notruf und f\u00fcr die Steuerung der Betriebszust\u00e4nde wurde durch Zustandsautomaten modelliert und daraus der Code f\u00fcr die Abl\u00e4ufe generiert. Entscheidend f\u00fcr den Erfolg war, dass die Automaten w\u00e4hrend der Entwicklung schrittweise erweitert und korrigiert werden konnten, weil sich der neu generierte Code mit minimalem Aufwand integrieren lie\u00df.<\/p>\n Die resultierende Implementierung funktionierte von vornherein einwandfrei und war auch bei vielfachen Wiederholungen im Systemtest absolut stabil und zuverl\u00e4ssig. Da Modell und Code durch Konstruktion \u00fcbereinstimmten, lie\u00dfen sich Fragen zum Verhalten direkt aus dem Modell beantworten.<\/p>\n Das Beispiel zeigt, dass es auch bei Entwicklungen auf der Basis eines vorhandenen Systems m\u00f6glich und lohnend ist, neue Teile modellbasiert zu entwickeln. F\u00fcr die Umsetzung ist folgende Vorgehensweise zu empfehlen:<\/p>\n Neben dem \u00fcberschaubaren Risiko beim \u00dcbergang zu modellbasierter Entwicklung hat diese Vorgehensweise den Vorteil, dass die Entwickler langsam an die neue Entwicklungsmethodik herangef\u00fchrt werden und so eventuelle Vorbehalte leichter \u00fcberwunden werden k\u00f6nnen.<\/p>\n Im zweiten Teil wurde die Simulation und formale Verifikation des Zustandsautomaten f\u00fcr die Steuerung der Betriebszust\u00e4nde mit Spin vorgestellt und dabei auf einige Besonderheiten der Methode eingegangen. Die Verhaltens\u00adbeschreibungen in Spin sind durch die Abstraktion einerseits recht kompakt und andererseits nahe genug an der Implementierung, um f\u00fcr diese g\u00fcltige Aussagen zu treffen.<\/p>\n Mit Spin ist ein Werkzeug verf\u00fcgbar, das sich f\u00fcr die formale Verifikation von realen Systemen eignet und nicht nur f\u00fcr kleine Beispiele. Wer also bei der \u00dcberpr\u00fcfung von Zustandsautomaten \u00fcber Reviews und ausgefeilte Tests hinausgehen will, kann mit Spin das Verhalten durch Simulation und durch formale Verifikation \u00fcberpr\u00fcfen und dabei Verklemmungen, Zyklen ohne Fortschritt und unerw\u00fcnschtes Verhalten schon im Modell aufdecken und beheben.<\/p>\n [1]\u00a0 T. Steinert, G. R\u00f6\u00dfler, „Generation of realistic signalling traffic in an ISDN load test system using SDL User Models“, Proceedings of FORTE\/PSTV 2000, Pisa.<\/p>\n [2]\u00a0 Spin Webseite.\u00a0https:\/\/spinroot.com\/<\/a><\/p>\n [3]\u00a0 M. Ben-Ari, „A Primer on Model Checking“, ACM Inroads 2010 March, Vol. 1, No. 1. Verf\u00fcgbar unter Beitrag als PDF downloaden<\/strong><\/a><\/p>\n Wollen Sie sich auf den aktuellen Stand der Technik bringen?<\/strong><\/p>\n Dann informieren Sie sich\u00a0hier<\/strong>\u00a0<\/a>zu Schulungen\/ Seminaren\/ Trainings\/ Workshops und individuellen Coachings von MircoConsult zum Thema Modellierung \/Embedded- und Echtzeit-Softwareentwicklung.<\/p>\n Training & Coaching zu den weiteren Themen unseren Portfolios finden Sie\u00a0hier<\/a>.<\/strong><\/p>\n Wertvolles Fachwissen zum Thema Modellierung \/Embedded- und Echtzeit-Softwareentwicklung steht\u00a0hier<\/strong>\u00a0<\/a>f\u00fcr Sie zum kostenfreien Download bereit.<\/p>\nSteuerger\u00e4t f\u00fcr ERA-GLONASS-Notruf<\/h2>\n
Codegenerierung aus dem Zustandsautomaten<\/h2>\n
\n
Simulation von Zustandsautomaten in UML<\/h2>\n
\u00dcbertragung der Zustandsautomaten nach\u00a0Spin<\/em><\/h2>\n
Simulatin und Verifikation mit\u00a0Spin<\/em><\/h2>\n
Zusammenfassung und Empfehlungen<\/h2>\n
\n
Referenzen<\/h2>\n
\nhttps:\/\/spinroot.com\/spin\/Doc\/p40-ben-ari.pdf<\/a><\/p>\n
\nModellierung – MicroConsult Trainings & Coachings<\/h2>\n
\nModellierung – Fachwissen<\/h2>\n