DiRePro: Directed Model Checking in the Analysis of Reactive and Probabilistic Systems
Participation in the AVACS projects S3 and R3
-->Project Summary
The complexity of embedded software systems calls for efficient automated methods that ensure that these systems satisfy correctness criteria ensuring safe operation. Important classes of properties that these systems have to meet relate to their real-time behavior, and to the probability of performing certain services within a given time period. In this project we contribute to the development of automated verification methods that allow these properties to be checked for a given software design model. The particular challenge is to ensure that these methods scale to the huge size of the sate spaces that concurrent embedded systems entail. We address this challenge by reconciling model checking techniques for real-time and probabilistic systems with heuristics directed, intelligent state space traversal techniques, also known as directed model checking. In particular, we use heuristic techniques to increase the efficiency of the abstraction refinement loop for real-time model checking, and to elicit meaningful error traces for probabilistic system models.
Zusammenfassung
Die Komplexität eingebetteter Softwaresysteme verlangt nach effizienten, automatischen Methoden die überprüfen, ob diese Systeme Korrektheitsanforderungen erfüllen, die ihr sicheres Funktionieren gewährleisten. Wichtige Klassen von Eigenschaften, die diese Systeme zu erfüllen haben, beziehen sich auf das Echtzeitverhalten dieser Systeme, und auf die Wahrscheinlichkeit, einen gewissen Dienst innerhalb einer vorgegebenen Zeitspanne zu erbringen. In diesem Projekt entwickeln wir automatische Verifikationsmethoden die es erlauben, solche Eigenschaften für ein gegebenes Entwurfmodell zu überprüfen. Die besondere Herausforderung liegt dabei darin, sicher zu stellen, dass sich diese Methoden auf die immense Größe der von nebenläufigen, eingebetteten Softwaresystemen erzeugten Zustandsräume skalieren lassen. Wir gehen diese Herausforderung insbesondere dadurch an, dass wir Modellprüfverfahren für Echtzeit- und probabilistische Systeme mit heuristischen, intelligenten Techniken der Zustandsraumanalyse verbinden. Diese Ansatz ist unter dem Begriff Gerichtete Modellprüfverfahren bekannt geworden. Insbesondere verwenden wir heuristische Techniken, um die Effizienz der Abstraktionsverfeinerung für Echtzeit-Modellprüfverfahren zu erhöhen, und um bedeutungsvolle Gegenbeispiele für probabilistische Systemmodelle zu finden.
This project is carried out in collaboration with the subprojects S3 an R3 of the Transregional Collaboration Research Center (Transregio-SFB) AVACS, in which the Chair for Software Engineering is an associate member.
Funding
Deutsche Forschungsgemeinschaft
Duration
2005-2008
Publications
- Husain Aljazzar, Holger Hermanns, and Stefan Leue: Counterexamples for Timed Probabilistic Reachability, Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems FORMATS'05, Lecture Notes in Computer Science, Springer Verlag. To appear, 2005. (PDF)
- Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability, Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS '06, Lecture Notes in Computer Science, Springer Verlag, 2006. (PDF)