CASPA is a stochastic process algebra tool for performance and dependability modelling, analysis, and verification. It is based entirely on the symbolic data structure of the multi-terminal binary decision diagram (MTBDD) which enables the tool to handle models with very large state space. This paper describes an extension of CASPA’s solving engine for path-based approximation of the mean time to first failure, the mean time to first recovery, and asymptotic unavailability by MTBDD algorithms. A non-trivial case study illustrates the use of path-based analysis and comparisons between the path-based unavailability calculations and results obtained from standard Markovian analysis are presented.
BouissouM.LefebvreY.A path-based algorithm to evaluate asymptotic unavailability for large Markov models. In Proceedings of the Annual reliability and maintainability symposium, Seattle, WA, USA, 28–31 January 2002, pp. 32–39 (IEEE, Piscataway, New Jersey).
2.
WernerE.Leistungsbewertung mit multi-terminalen binären entscheidungsdiagrammen. MSc Thesis, Computer Science 7, Universität Erlangen, 2003.
3.
KuntzM.SiegleM.WernerE.Symbolic performance and dependability evaluation with the Tool CASPA. Lect. Notes Comput. Sci., 2004, 3236, 293–307.
4.
BachmannJ.RiedlM.SchusterJ.SiegleM.An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA. Lect. Notes Comput. Sci., 2009, 5404, 485–496.
5.
WalterM.SiegleM.BodeA.OpenSESAME: the simple but extensive, structured availability modeling environment. Reliab. Engng. Sys. Saf., 2007, 93(6), 857–873.
6.
GüntherM.SchusterJ.SiegleM.Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA. In Proceedings of the First Workshop on Dynamic aspects in dependability models for fault-tolerant systems, Valencia, Spain, 27 April 2010, pp. 13–18 (The Association for Computing Machinery, New York, USA).
7.
AzevedoJ.MadeiraJ.MartinsE.PiresF.A shortest paths ranking algorithm. In Proceedings of the Annual conference of the Operations Research Society of Italy, Sorrento, Italy, October 1990. pp. 1001–1011 (IEEE Piscataway, USA.).
8.
SchmidW.Berechnung kürzester wege in straßennetzen mit wegeverboten. PhD Thesis, Fakultät für Bauingenieur- und Vermessungswesen, Universität Stuttgart, 2000.
9.
BouissouM.BonJ.-L.A new formalism that combines advantages of fault-trees and Markov models: Boolean logic driven Markov processes. Reliab. Engng. Syst. Saf., 2003, 82, 149–163.
