RigorOus dependability analysis using model ChecKing techniques for Stochastic systems (ROCKS)
Final Report Abstract
The bilateral DFG-NWO project ROCKS supported the collaboration between the formal-methods groups at the RWTH Aachen, TU Dresden, University of the Federal Armed Forces Munich and Saarland University on the German side and the Radboud Universiteit Nijmegen and Universiteit Twente on the Dutch side. The main achievements of ROCKS have been contributions to develop the foundations of dependability engineering using stochastic operational models and sophisticated model-checking techniques for the quantitative system analysis and related synthesis problems. During the funding period of ROCKS, the consortium developed a portfolio of modelling and abstraction techniques, and algorithms for the analysis of stochastic models as well as prototype implementations thereof. Major achievements in the direction of compositional reasoning are the development of the theory of Markov automata and various modelling and abstraction approaches for stochastic timed/hybrid automata, including hybrid variants of the modelling language MoDeST, as well as stochastic Petri nets. Preeminent contributions for the analysis are new algorithms for the generation of counterexamples as an indication for “critical subsystems”, for the parameter synthesis and for a trade-off analysis between cost and utility requirements. To tackle the state-explosion problem, the ROCKS consortium studied, among others, counterexample-guided abstraction-refinement algorithms, mean-field theoretic model-checking techniques and symbolic approaches with variants of zero-surpressed binary decision diagrams. A wide range of the developed concepts have been implemented and made available as stand-alone software tools or integrated in tools developed elsewhere. The most prominent one is MRMC, which is a generic probabilistic model checker for Markov chains that has been developed in u cooperation of the ROCKS groups in Aachen, Saarbrücken and Twente. Other tools developed by ROCKS members are COMICS (for the generation of counterexamples), FORTUNA (a model checker for probabilistic priced timed automata), PARAM (a probabilistic model checker for parameterized models), PASS (a probabilistic model checker that uses predicate abstraction for an iterative counterexampleguided abstraction-refinement approach), MoDeS (a discrete-event simulator for stochastic systems modelled in the MoDeST framework) and LARES (a tool for modelling and analysing reconfigurable dependable systems). These tools served as base not only for empirical scalability studies by means of academic benchmark examples, but also for demonstrating the feasibility of probabilistic model checking in challenging application areas. The dependability and survivability analysis of a water supply process is an impressive example for the general applicability of the concepts developed by ROCKS in the area of resource-critical infrastructures. Other examples include the analysis of energy-aware resource management systems, the quantitative evaluation of routing and load balancing protocols in sensor networks, and the synthesis of optimal battery policies for e-bikes. Besides regular, yet very intensive project meetings at varying locations in the Netherlands and in Germany, the ROCKS consortium organised an autumn school in October 2012 in South Tyrol with 10 tutorials on ROCKS-related topics given by international guest speakers and a few ROCKS members. The ROCKS school proceedings with contributions by doctoral students have been published as volume 8453 of Springer’s Lecture Notes in Computer Science.
Publications
- Evaluating repair strategies for a water-treatment facility using Arcade. In Proc. of the 2010 IEEE/IFIP Int. Conf. on Dependable Systems and Networks (DSN’10), pages 419–424. IEEE Computer Society, 2010
Boudewijn R. Haverkort, Matthias Kuntz, Anne Remke, Stephan Roolvink, and Mariëlle e Stoelinga
- Partially-shared zerosuppressed multi-terminal BDDs: Concept, algorithms and applications. Formal Methods in System Design, 36(3):198–222, 2010
Kai Lampka, Markus Siegle, Joern Ossowski, and Christel Baier
- Performability assessment by model checking of Markov reward models. Formal Methods in System Design, 36(1):1–36, 2010
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen
- Synthesis and stochastic assessment of cost-optimal schedules. International Journal on Software Tools for Technology Transfer, 12(5):305–318, 2010
Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, and Holger Hermanns
- The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 68(2):90–104, 2011
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, and David N. Jansen
- Probabilistic ω-automata. Journal of the ACM, 59(1), 2012
Christel Baier, Nathalie Bertrand, and Marcus Größer
- Three-valued abstraction for probabilistic systems. Journal on Logic and Algebraic Programming, 81(4):356–389, 2012
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf
- Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems - International Autumn School, ROCKS 2012, Vahrn, Italy, October 22-26, 2012, Advanced Lectures, volume 8453 of LNCS. Springer, 2014
Anne Remke and Mariëlle Stoelinga, editors
(See online at https://dx.doi.org/10.1007/978-3-662-45489-3) - Symbolic counterexample generation for large discrete-time Markov chains. Science of Computer Programming, 91(A):90–114, 2014
Nils Jansen, Ralf Wimmer, Erika Abrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, and Johann Schuster
(See online at https://doi.org/10.1016/j.scico.2014.02.001)
