Subproject

S3

Categories

Model reduction, Model checker / solver for probabilistic systems

Overview

The "Dependability Evaluation for STATEMATE" (DES) tool chain is a (plug-in) extension of STATEMATE enabling the evaluation of quantitative dependability properties at design time. Given a model specification provided by the user that consists of (i) the STATEMATE description, (ii) a list of timed (or failure) events and, for each event, (iii) the probabilistic timing information, DES allows to verify timed reachability properties such as "The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01".

MCSI extends the DES tool chain by an intermediate processing step that encodes path information into the models state space given a labeled transition system (LTS). This enables to relate all relevant paths leading to any safety critical state to a given particular minimal cut set (MCS) of failure events -- and by this to compute the contribution of a MCS to the overall probability of hitting a safety-critical state.

Publications

E. Böde, T. Peikenkamp, J. Rakow, and S. Wischmeyer. Model based importance analysis for minimal cut sets. In Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan, editors, 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 5311 of Lecture Notes in Computer Science (LNCS), pages 303-317, 2008.

Benchmarks

ETCS Application Level 2

Download

Click here for binary & manual.

Manual

(see above)

Status

Proof of concept