AVACS

DRESISP
AVACS
MEALS
SENSATION
ROCKS

AVACS is a Transregional Collaborative Research Center sponsored by the German Research Foundation DFG. AVACS is devoted to foundational research on Automated Verification and Analysis of Complex Systems. Research within AVACS is subdivided in three project areas named R (Real time), H (Hybrid) and S (no, not Stochastic, but Coarse Grain System Structure). Click on the links to get a short description of each area.

 

The Dependable Systems and Software chair contributes to the subprojects H4 and S2, and plays a pivotal role in subproject S3. This subproject integrates quantitative dependability analysis with state of the art computer aided verification. This effort has two sides. On the modeling side, we will enable the formal specification of dependability models and dependability properties via high-level engineering design notations. On the analysis side, we strive for a considerable advancement of the currently available technology.

 

Model checking algorithms are being developed to allow the formal analysis of a broad spectrum of quantitative dependability models. The model checking algorithms are analyzing stochastic processes, calculating the probability with which certain dependability requirements hold. In particular, we extend the class of checkable models from simple Markov models towards models with nondeterminism and towards classes of non-Markov processes. Advanced techniques will be developed enabling the efficient analysis of stochastic processes and decision processes of a very general nature. The envisaged algorithmic advances rely on joint efforts in the context of symbolic (BDD based) data structures and of directed model checking heuristics. Our techniques will be incorporated and tailored to hierarchical design notations, especially statecharts, and will be embedded in an engineering context where fault trees play a vital role, and therefore receive distinguished attention in the subproject. A software platform will be realized to conduct case studies of realistic size in the context of the upcoming European Train Control Systems standard.