Timed Model-Checking for Time-Triggered System Designs
Final Report Abstract
Verteilte Realzeitsysteme verwenden oft Prinzipien der Time-Triggered Architecture, um Konflikte beim Zugriff auf gemeinsame Ressourcen zu reduzieren. Ein Beispiel ist die Kommunikation in drahtlosen Sensornetzwerken (wie etwa funkbasierten Brandmeldeanlagen), in denen es zum Verlust von Nachrichten kommen kann, wenn mehrere Komponenten auf das gemeinsame Medium senden. Das Risiko für Nachrichtenkollisionen kann durch Time-Triggered Designs verringert werden, in denen zu jedem Zeitpunkt festgelegt ist, welche Komponente senden darf. Sicherheitskritische, eingebettete Systeme wie Brandmeldeanlagen sollen über lange Zeiträume zuverlässig und energieeffizient arbeiten, wobei aus Gründen der Energieeffizienz oft individuell entwickelte Funkprotokolle verwendet werden. Die Zuversicht in die Korrektheit der Funkprotokolle kann durch Modell-basierte Entwicklung erhöht werden, bei der Design-Ideen in einem abstrakten, formalen Modell dargestellt werden und das Modell mit Hilfe des Timed Model-Checking automatisch daraufhin analysiert wird, ob z.B. alle relevanten Zeitschranken eingehalten werden. Der bekannte Timed Model-Checking-Algorithmus ist u.a. komplex in der Anzahl Uhren(variablen) im Modell, mit deren Hilfe kontinuierliche Zeit modelliert wird. Speziell für Modelle verteilter Realzeitsysteme ergibt sich dabei der folgende Zielkonflikt: Um gut validierbar zu sein, um also mit Domänenexperten aus dem Bereich des Time-Triggered Designs zu diskutieren, ob die Design-Ideen korrekt im Modell dargestellt sind, sollte im Modell sichtbar sein, dass im verteilten System jede Komponente einen eigenen Zeitgeber hat. Zeitgeber werden durch Uhren dargestellt und durch viele Uhren im Modell kann die Analyse in gegebenen Zeit- oder Speichergrenzen unpraktikabel werden. Protokollzeit im Modell durch zentrale Zeitgeber darzustellen kann den Aufwand für die Analyse verringern, erhöht jedoch das Risiko für Missverständnisse bei der Validierung und für Fehler bei Änderungen des Modells. Eine Lösung für diesen Konflikt verspricht die Quasi-Equal Clock Reduction, bei der gut validierbare Ausgangsmodelle mit quasi-gleichen Uhren in für die Analyse optimierte Modelle transformiert werden. Zwei Uhren sind quasigleich, wenn ihre Werte in jeder erreichbaren Konfiguration des Modells gleich sind oder eine der Uhren den Wert 0 hat, und finden sich besonders häufig in Modellen von verteilten Realzeitsystemen mit Time-Triggered Designs. Dank der Quasi-Equal Clock Reduction muss nur noch das gut validierbare Ausgangsmodell gepflegt werden, während die Transformation automatisch ein effizient analysierbares Modell liefert. Im Projekt wurden im Bereich der Quasi-Equal Clock Reduction für das Timed Model-Checking von Time-Triggered Designs die folgenden Fortschritte erzielt. Die bisherige Darstellung der Quasi-Equal Clock Reduction in der Literatur folgte der schrittweisen Entwicklung des Verfahrens mit Vereinfachungen oder Verkürzungen zugunsten der jeweils neuen Schritte. Als Ergebnis des Projekts liegt eine geschlossene Darstellung der Theorie der Quasi-Equal Clock Reduction vor, die Unklarheiten in seltenen Randfällen beseitigt und insgesamt den Korrektheitsbeweis und die Arbeit mit dem Verfahren vereinfacht. Die Quasi-Equal Clock Reduction ist besonders effektiv für Ausgangsmodelle mit Kanten, die die sogenannte Simple Edge-Eigenschaft haben, die durch eine Kombination von syntaktischen und semantischen Kriterien definiert ist. Das semantische Kriterium für Simple Edges ist sogenanntes pre- und post-Delay, das intuitiv fordert, dass die Ausgangsund End-Locations der Kante nicht verlassen werden können ohne dass eine positive Zeit verstreicht. Bisher existierten nur hinreichende syntaktische Kriterien für pre- und post-Delay. Im Rahmen des Projekts wurde ein neues approximatives Analyseverfahren entwickelt, für das Präzision und Aufwand durch die Wahl eines Analyse-Horizonts beeinflussbar sind. In der Evaluation konnten mit kleinen Analyse-Horizonten in kurzer Zeit Kanten mit den gesuchten Eigenschaften erkannt werden. Die wichtigste Information für Quasi-Equal Clock Reduction ist, welche Uhren im Ausgangsmodell quasi-gleich sind. Auch quasi-Gleichheit ist eine semantische Eigenschaft, und bisher existierte nur eine unvollständige statische Analyse, die zusätzlich zur Transformation und zur Analyse des transformierten Modells durchzuführen ist. Im Rahmen des Projekts wurde ein neuer Timed Model-Checking-Algorithmus entwickelt, der die Erkennung und Nutzung quasi-gleicher Uhren in einem Analyselauf integriert, mit gleichem Speicherbedarf wie die Analyse des transformierten Modells bisher. Beide neuen Verfahren wurden in einem im Rahmen des Projekts entwickelten Framework zur Transformation und Analyse von Timed Automata implementiert, das jetzt als Open-Source Software zur Verfügung steht. Im weiteren Sinne des Timed Model-Checking für Time-Triggered Designs wurden im Rahmen des Projekts Fortschritte im Bereich der Analyse von gezeiteten reflektiven Beschreibung von Realzeit-Anforderungen erzielt, sowie ein wichtiger Schritt hin zur Generierung von Code für verteilte Realzeitsysteme mit Korrektheitsgarantien unternommen. Reflektive Beschreibungen spezifizieren nur das beobachtbare Verhalten von Systemen, während konstruktive Beschreibungen angeben, wie das beobachtbare Verhalten entsteht. Relevante und im Projekt bearbeitete Analysefragen für reflektive Beschreibungen sind Konsistenz oder rt-Konsistenz, eine Anwendung für reflektive Beschreibungen ist die Spezifikation der Zeitschranken, die für ein Design-Modell mit Timed Model-Checking zu prüfen sind. Die Generierung von Code aus abstrakten, formalen Modellen ist für viele Modellierungssprachen möglich, jedoch oft mit nur schwachen Aussagen darüber, welche Korrektheitseigenschaften des Modells sich auf das Programm übertragen. Im Rahmen des Projekts wurde ein neuer Vorschlag für die Generierung von Code für den anspruchsvollen Fall verteilter Realzeitsysteme entwickelt, bei dem Garantien für Korrektheitseigenschaften des Codes gegeben werden können. Eine Voraussetzung für das neue Verfahren sind Modelle von Time-Triggered Designs auf einem passenden Abstraktionslevel, also genau solche Modelle wie sie bei der Quasi-Equal Clock Reduction als Ausgangsmodelle betrachtet werden.
Publications
- Scalable analysis of real-time requirements. In Daniela E. Damian, Anna Perini, and Seok-Won Lee, editors, 27th IEEE International Requirements Engineering Conference, RE 2019, Jeju Island, Korea (South), September 23-27, 2019, pages 234–244. IEEE, 2019
Vincent Langenfeld, Daniel Dietsch, Bernd Westphal, Jochen Hoenicke, and Amalinda Post
(See online at https://doi.org/10.1109/re.2019.00033) - Formal requirements in an informal world. In Sophie Ebersold, Régine Laleau, and Manuel Mazzara, editors, Formal Requirements 2020, FormReq 2020, Zurich, August 31, 2020, Proceedings, pages 14–20. IEEE, 2020
Daniel Dietsch, Vincent Langenfeld, and Bernd Westphal
(See online at https://doi.org/10.1109/formreq51202.2020.00010) - On implementable timed automata. In Alexey Gotsman and Ana Sokolova, editors, Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, volume 12136 of Lecture Notes in Computer Science, pages 78–95. Springer, 2020
Sergio Feo Arenis, Milan Vujinovic, and Bernd Westphal
(See online at https://doi.org/10.1007/978-3-030-50086-3_5) - Hanfor: Semantic requirements review at scale. In Fatma Basak Aydemir, Catarina Gralha, Maya Daneva, et al., editors, Joint Proceedings of REFSQ 2021 Workshops, OpenRE, Poster and Tools Track, and Doctoral Symposium co-located with the 27th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2021), Essen, Germany, April 12, 2021, volume 2857 of CEUR Workshop Proceedings. CEUR-WS.org, 2021
Samuel Becker, Daniel Dietsch, Nico Hauff, Elisabeth Henkel, Vincent Langenfeld, Andreas Podelski, and Bernd Westphal
- Quasi-equal clock reduction on-the-fly. In Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez, editors, NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings, volume 12673 of Lecture Notes in Computer Science, pages 375–391. Springer, 2021
Bernd Westphal
(See online at https://doi.org/10.1007/978-3-030-76384-8_23)
