Quantitative Timed Analysis of Interactive Markov Chains

Organisation:	RWTH Aachen and Saarland University (GERMANY) University of Oxford (UNITED KINGDOM)
Functionality:	Quantitative analysis of Interactive Markov chains
Tools used:	GNU Multiple Precision Arithmetic Library Multiple Precision Floating-Point Reliable Library (MPFR) QT and SoPlex libraries CADP (Construction and Analysis of Distributed Processes)
Period:	2012
Description:	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.
Conclusions:	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.
Publications:	[Guck-Han-Katoen-Neuhaeusser-12] 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 the CADP Web site in PDF or PostScript
Contact:	Prof. Dr. Ir. Joost-Pieter Katoen RWTH Aachen University LS2: Software Modeling and Verification D-52056 Aachen Germany Tel: +49 (241) 8021200 Fax: +49 (241) 8022217 Email: katoen@cs.rwth-aachen.de
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page