Path-based calculation of MTTFF, MTTFR, and asymptotic unavailability with the stochastic process algebra tool CASPA

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.