RigorOus dependability analysis using model ChecKing techniques for Stochastic systems

DFG logo blue  NWO logo

Summary of the Project

Today's society relies increasingly on the correct and timely functioning of a large variety of information and communications technology systems. Can this reliance be justified? Dependability analysis aims to answer this question. Rigorous and systematic dependability analysis ("Dependability Engineering") must therefore play an important role in the design of such systems. Since many dependability properties are stochastic in nature, stochastic analysis techniques are crucial in developing reliable computer systems. The ROCKS project will focus on two system classes which are gaining prominence in the world of computing but which are not amenable to classic stochastic analysis techniques. Large scale homogeneous systems, such as wireless sensor networks and gossiping protocols, provide a challenge because standard (compositional) approaches for large systems fail in this case. Safetycritical heterogeneous systems, such as production plants and automotive control systems, on the other hand consist of a number of very different components. The challenge here is to handle the diversity of system modalities. We will study how, given a system configuration or parameter set, the optimal design can be synthesised automatically. Attention will also be given to the study of architectural description languages which are increasingly being used to describe complex systems, but for which analysis techniques are often lacking. The seven applying research groups each have a proven record in neighbouring research areas. Their cooperation, supported by this project, can thus be expected to lead to synergetic effects, which will bring the development of "Dependability engineering" a large step forward.

The goals of the ROCKS project are:

  • extend architectural description languages, like AADL and UML, such that these models can be analysed by stochastic model checking techniques;
  • strengthen the core technological, methodological and foundational aspects of stochastic model checking, so that they can be applied to large scale homogeneous systems as well as safety-critical heterogeneous systems,
  • exploit the expertise in analysis of stochastic systems to move towards synthesis and optimisation techniques.

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