Timed Model-Checking für Time-Triggered Systemdesigns

• Antragsteller: Dr. Bernd Westphal
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2017 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 385729514

Das Ziel des hier vorgeschlagenen Projekts ist die Weiterentwicklung des Stands der Technik im Model-Checking für Realzeitsysteme. Realzeitsysteme können mit Hilfe von Netzwerken gezeiteter Automaten (Alur & Dill, 1994) modelliert und verifiziert werden. Das Model-Checking von Systementwürfen für Realzeitsysteme gewinnt zunehmend Aufmerksamkeit in der High-Tech Industrie, sogar in kleinen und mittleren Unternehmen (KMU). Obwohl Werkzeuge wie Uppaal über die Zeit stetig verbessert wurden, ist das bekannte State-Explosion-Problem weiterhin ein signifikantes Hindernis bzgl. der weiten Verbreitung dieser Technologie.Das Projekt wird auf aktive Forschungsarbeiten aufbauen, insbesondere auf eigene Vorarbeiten. In eigenen Vorarbeiten haben wir den Begriff der quasi-gleichen Uhren eingeführt. Quasi-gleiche Uhren treten insbesondere in Entwürfen verteilter Systeme, die eine Time-Triggered Architektur verwenden, z.B. in Form des bekannten Time Division Multiple Access (TDMA) Schemas zum Zeitmultiplexing. Wir haben ein Werkzeug namens saset entwickelt, das eine Source-to-Source-Transformation von Netzwerken gezeiteter Automaten implementiert, die QE-Transformation. Gegeben ein Originalnetzwerk mit quasi-gleichen Uhren liefert saset ein transformiertes Netzwerk in dem alle Uhren einer Äquivalenzklasse bzgl. Quasi-Gleichheit durch eine einzelne Repräsentanten-Uhr ersetzt worden sind. Für viele industrielle Fallstudien aus der Literatur und aus eigenen Projekten konnten wir durch den Einsatz der QE-Transformation signifikante Verringerungen der Anzahl von Uhren im Modell und des für Model-Checking Aufgaben notwendigen Rechenaufwands beobachten.Das hier vorgeschlagenen Projekt umfasst drei Themenbereiche:(1) Die Untersuchung von Komplexitätsaspekten und, ausgehend von entsprechenden Resultaten, eine weitere Verbesserung der QE-Transformation.(2) Die automatische und effiziente Erkennung von bestimmten Kanten für welche die QE-Transformation am effektivsten arbeitet.(3) Die Entwicklung eines neuen Model-Checking Verfahrens, in dem die Inferenz von Quasi-Gleichheit und die QE-Transformation eng verzahnt sind.Die Contributions des Projekts werden theoretischer und praktischer Natur sein. Wir werden ein tieferes Verständnis des Potentials und der Grenzen der QE-Transformation erhalten. Wir werden ein Werkzeug als Erweiterung von saset entwickeln, das eine verbesserte QE-Transformation implementieren wird, das ein Modul zur Inferenz von unabhängigen Kanten enthalten wird, sowie eine Implementierung des neuen Model-Checking Verfahrens. Die Werkzeuge werden der wissenschaftlichen Community zur Verfügung gestellt werden.

• DFG-Verfahren: Sachbeihilfen