RWTH Aachen and Saarland University (GERMANY)
University of Oxford (UNITED KINGDOM)
Quantitative analysis of Interactive Markov chains
GNU Multiple Precision Arithmetic Library
Multiple Precision Floating-Point Reliable Library (MPFR)
QT and SoPlex libraries
CADP (Construction and Analysis of Distributed Processes)
Continuous-time Markov chains (CTMCs) are a widely-studied stochastic
model in performance evaluation and naturally reflect the random
real-time behavior of stoichiometric equations in systems biology.
Labeled transition systems (LTSs) are one of the main operational
models for concurrency and are equipped with a plethora of behavioral
equivalences like bisimulation and trace equivalences. A natural
mixture of CTMCs and LTSs yields so-called interactive Markov chains
(IMCs), originally proposed as a semantic model of stochastic process
algebras. IMCs are an appropriate semantic backbone for several
formalisms, such as stochastic process algebras, dynamic fault trees
(DFTs), and the standardized Architectural Analysis and Design
Language (AADL) in which nominal system behavior is extended with
probabilistic error models. The CADP toolbox supports the compositional
generation, minimization, and standard CTMC analysis of IMCs.
This work proposes novel features for the quantitative timed analysis of arbitrary (in particular, non-deterministic) IMCs, namely for computing the expected time analysis and long-run average fraction of time analysis, both of which can be reduced to stochastic shortest path (SSP) problems. These algorithms have been implemented in the IMCA (IMC Analyzer) tool, which supports the verification of IMCs against (a) timed reachability objectives, (b) reachability objectives, (c) expected time objectives, (d) expected step objectives, and (e) long-run average objectives. IMCA supports the BCG format for LTSs, being a useful back-end for the CADP toolbox, as well as for analysis tools for DFTs and AADL error models. The scalability of the approach is illustrated on two examples: a dependable workstation cluster and a Google file system.
As IMCs are the semantic backbone of engineering formalisms such as
AADL error models, DFTs, and GALS hardware designs, the IMCA tool
enlarges the analysis capabilities for dependability and reliability.
The support of the compressed BCG-format allows for the direct usage
of IMCA as back-end to tools like CADP and CORAL.
Dennis Guck, Tingting Han, Joost-Pieter Katoen, and
Martin R. Neuhaeusser.
"Quantitative Timed Analysis of Interactive Markov Chains".
Proceedings of the 4th International Symposium on NASA Formal Methods
NFM'2012 (Norfolk, VA, USA), Lecture Notes in Computer Science vol.
7226, pp. 8-23. Springer Verlag, April 2012.
Available on-line at: ftp://ftp.informatik.rwth-aachen.de/pub/publications/rwth/informatik/2012/2012-09.pdf
or from our FTP site in PDF or PostScript
Prof. Dr. Ir. Joost-Pieter Katoen
RWTH Aachen University
LS2: Software Modeling and Verification
Tel: +49 (241) 8021200
Fax: +49 (241) 8022217
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|