DES
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". DES is the result of a truly transregional effort, among others, it encompasses the following tools:  stm2lts, a Statemate plugin, that extracts a labeled transition system (BDD based representation, XML)  sigref that applies aggressive symbolic (BDD based) minimization on the LTS  imc2ctmdp that transforms the LTS enriched by stochastic time constraints, given as interactive Markov chains (IMCs), into a uniform CTMDP. DES requires the following external tools and frameworks:  Statemate  CADP  MRMC 
E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp, R. Pulungan, J. Rakow, R. Wimmer, and B. Becker. Compositional dependability evaluation for Statemate. IEEE Transactions on Software Engineering, 35(2):274292, 2009. 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 