DES
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". DES is the result of a truly trans-regional effort, among others, it encompasses the following tools: - stm2lts, a Statemate plug-in, 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):274-292, 2009. 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. |
|
ETCS Application Level 2 |
|
Download |
Click here for binary & manual. |
Manual |
(see above) |
Status |
Proof of Concept |