MCSI  Minimal Cut Sets Importance Analysis
Subproject 
S3 
Categories 
Model reduction, Model checker / solver for probabilistic systems 
Overview 
The "Dependability Evaluation for STATEMATE" (DES) tool chain is a (plugin) 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 safetycritical 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 safetycritical state. 
E. Böde, T. Peikenkamp, J. Rakow, and S. Wischmeyer. Model based importance analysis for minimal cut sets. In Sung Deok Cha, JinYoung 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 303317, 2008. 

ETCS Application Level 2 

Download 
Click here for binary & manual. 
Manual 
(see above) 
Status 
Proof of concept 