• Introduction
• Summary
• Research Programme
• Participants
• Meetings
• Publications

RigorOus dependability analysis using model ChecKing techniques for Stochastic systems

Research Programme

1. Modelling. To apply stochastic model checking techniques to analyse dependability properties of system designs expressed in ADLs, we will derive stochastic models automatically from (an expressive subset of) AADL or UML. Since existing stochastic models cannot express all features included in ADLs (especially those required in safety-critical heterogeneous systems), we will enrich these models with new modalities. In particular, we will work on hierarchical modelling constructs and on stochastic models combining various modalities (discrete and continuous distributions, stochastic and deterministic time). Our key concern will be the balance between expressiveness and analysability of these enriched formalisms.
2. Analysis. Efficiency improvements in analysis techniques are fundamental to give an answer to the ever-increasing complexity of the systems under scrutiny. ROCKS will therefore improve existing symbolic techniques for stochastic model checking, and re-develop algorithms to exploit modern multi-core processor architectures. Moreover, more aggressive abstractions of stochastic systems will be developed. These improved methods will allow larger system models to be analysed. For large-scale homogeneous systems this will, however, not always do. ROCKS will therefore investigate cutting-edge techniques like mean field theory and so-called spotlight principles.
3. Synthesis. Optimal control and synthesis problems have a long history in the fields of operational research, AI, and planning. For a decade now, they have gained the attention of the model checking community. Approaches to exploit stochastic model checking techniques for synthesis do exist already. Compared to classical optimisation, model checking-based techniques offer
   1. powerful system modelling languages, such as ProbMela and the PRISM-input language, facilitating the creation of complex system models;
   2. powerful property specification languages, such as probabilistic LTL, PCTL, and CSL, to express a variety of system properties;
   3. and the inherent possibility to derive parameters, control sequences or schedules that optimise the behaviour of the modelled system.
   ROCKS will work on counterexamples for stochastic model checking, synthesis methods for stochastic systems expressed as continuous-time MDPs (Markov decision processes) as well as partially observable MDPs, and parameter synthesis methods for stochastic models.
4. Application areas. The following application areas serve as motivators for the techniques to be developed and shall provide concrete case-studies with which the applicability of the methods devised during ROCKS is assessed.
   1. Critical infrastructures. In the class of safety-critical heterogeneous systems, we shall analyse and optimise safe and cost-optimal schedules in safety-critical infrastructures and production systems.
   2. Wireless sensor networks. In the class of large scale homogeneous networks, we shall analyse the performance and dependability of wireless sensor networks. Key concerns are low-power computation characteristics and reliable communication.
   3. Energy resource modelling. In this area, we shall synthesise power-optimal usage profiles for batteries, requiring relatively small, but sophisticated Markovian models.

ROCKS is a cooperation of RWTH Aachen, TU Dresden, UT-DACS Enschede, UT-FMT Enschede, UBwM Munich, RU Nijmegen and UdS Saarbrücken