Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems
Final Report Abstract
The proper functioning of embedded and cyber-physical systems is an essential objective in software and systems engineering. This is particularly true when those systems are safety-critical, which means that their malfunctioning may endanger the environment or human life. The design process relies on the specification of essential system properties, followed by an architectural design in which the functioning of different system components is developed. An essential system property could be, for instance, that an air bag in a car will not explode unless an accident actually has been detected. For many of these systems it is essential that they satisfy what is referred to as ”non-functional” system properties. Those are properties that rely, for instance, on real time bounds, such as ”the air bag shall be deployed no later than 50 ms after the detection of a crash”. Since many safety-critical systems are not entirely safe, what is often required are probabilistic timed guarantees, such as ”the probability of the airbag being deployed even if no crash has been detected is smaller than 10^−9 per hour of operation.” As a consequence, the focus of the work in this research project has been on developing automated verification technology which checks whether such probabilistic timed properties are actually guaranteed by the architectural design of the model. The technology that we develop is based on model checking, which is a complete and terminating procedure inspecting all possible configurations, here called states, of the system. It is automatic because once the specification is formulated and the architectural design is modeled, the procedure executes without any further user interaction. This makes model checking based technology a prime candidate for inclusion into practical system design processes. While the model checking technology for those types of properties is well developed, we identified in the beginning of the project a dearth in computing explanations for the reason of a property violation. A probabilistic model checker will tell the user whether a property is valid or violated, but not provide an explanation why a violation occurs. The approach that we have developed in this project computes such explanations, which we refer to as counterexamples. They represent a set of executions of the system that start in its initial state and end in a state where the property is violated, e.g., where the airbag has been exploded without a crash having been detected beforehand. Since we are considering probabilistic properties, each such trace carries a probability of occurrence. Obviously, it is desirable to include those system traces into the counterexample for which the probability is highest, so that we obtain a good number of meaningful and very probable property violating traces in the counterexample. In order to achieve this goal we are using heuristics guided search algorithms, gleaned from the area of Artificial Intelligence, in computing the counterexample. The Algorithms that we consider are Best-First Search, Z* and A*. In particular, we consider the counterexample computation problem as an instance of the k-shortest-paths (KSP) problem. To solve this problem, we developed the K* algorithm, which is first and, at the time of writing, only heuristics guided, on-the-fly algorithm to solve the KSP problem. In addition to being very useful in the computation of counterexamples, it has many applications in other domains, for instance in route planning. In order to establish the applicability to real-life engineering problems we have applied this counterexample computation to an analysis of the architecture of an industrial air bag system architecture. Using the counterxample computation we could prove that for this example, using just one microprocessor for the signal processing would not suffice to achieve a legally required system dependability and that, hence, a second redundant microprocessor needed to be added. In subsequent research we have extended this approach to a comprehensive probabilistic safety analysis method leading to the automatic synthesis of probabilistic fault trees, a common engineering safety analysis notation.
Publications
- Counterexamples for timed probabilistic reachability. In FORMATS, volume 3829 of Lecture Notes in Computer Science, pages 177–195. Springer, 2005
Husain Aljazzar, Holger Hermanns, and Stefan Leue
(See online at https://doi.org/10.1007/11603009_15) - Extended directed search for probabilistic timed reachability. In FORMATS, volume 4202 of Lecture Notes in Computer Science, pages 33–51. Springer, 2006
Husain Aljazzar and Stefan Leue
(See online at https://doi.org/10.1007/11867340_4) - Partial-order reduction for general state exploring algorithms. In SPIN, volume 3925 of Lecture Notes in Computer Science, pages 271–287. Springer, 2006
Dragan Bosnacki, Stefan Leue, and Alberto Lluch-Lafuente
(See online at https://doi.org/10.1007/11691617_16) - Directed Model Checking, 26.04. - 29.04.2006, volume 06172 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany, 2007
Stefan Edelkamp, Stefan Leue, and Willem Visser, editors
- Automated predicate abstraction for real-time models. In INFINITY, volume 10 of EPTCS, pages 36–43, 2009
Bahareh Badban, Stefan Leue, and Jan-Georg Smaus
(See online at https://doi.org/10.4204/EPTCS.10.3) - Safety analysis of an airbag system using probabilistic FMEA and probabilistic counterexamples. In QEST, pages 299–308. IEEE Computer Society, 2009
Husain Aljazzar, Manuel Fischer, Lars Grunske, Matthias Kuntz, Florian Leitner-Fischer, and Stefan Leue
(See online at https://doi.org/10.1109/QEST.2009.8) - Automated invariant generation for the verification of real-time systems. In WING@ETAPS/IJCAR, volume 1 of EPiC Series in Computing, pages 44–58. EasyChair, 2010
Bahareh Badban, Stefan Leue, and Jan-Georg Smaus
- Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation. In QUO- VADIS@ICSE, pages 25–32. ACM, 2010
Husain Aljazzar, Matthias Kuntz, Florian Leitner-Fischer, and Stefan Leue
(See online at https://doi.org/10.1145/1808877.1808883) - Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Software Eng., 36(1):37–60, 2010
Husain Aljazzar and Stefan Leue
(See online at https://doi.org/10.1109/TSE.2009.57) - Dipro - A tool for probabilistic counterexample generation. In SPIN, volume 6823 of Lecture Notes in Computer Science, pages 183–187. Springer, 2011
Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue, and Dimitar Simeonov
(See online at https://doi.org/10.1007/978-3-642-22306-8_13) - K∗ : A heuristic search algorithm for finding the k shortest paths. Artif. Intell., 175(18):2129–2154, 2011
Husain Aljazzar and Stefan Leue
(See online at https://doi.org/10.1016/j.artint.2011.07.003)
