DiRePro: Directed Model Checking in the Analysis of Reactive and Probabilistic Systems
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.
Subprojects
- Heuristic Search and Abstract Model Checking for Real-Time Systems
- Formal Verification of Availability Properties
Funding
Deutsche Forschungsgemeinschaft
These projects correspond to our work packages in the R3 and S3 subprojects of the Transregional Collaboration Research Center (Transregio-SFB) AVACS, in which we where involved as a member throughout March 2004, and later as an associate member.
Duration
2005-2008