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.
- 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.
- 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
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.
- powerful system modelling languages, such as ProbMela and the PRISM-input language,
facilitating the creation of complex system models;
- powerful property specification languages, such as probabilistic LTL, PCTL, and CSL,
to express a variety of system properties;
- and the inherent possibility to derive parameters, control sequences or schedules that
optimise the behaviour of the modelled system.
- 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.
- 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.
- 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.
- 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