Compositional reliability analysis using probabilistic component automata

Compositionality is a key property in the development and analy- sis of component-based systems. In non-probabilistic formalisms such as Labelled Transition Systems (LTS) the functional behaviour of a system can be readily constructed from the behaviours of its parts. However, this is not true for probabilistic extensions of LTS, which are necessary to analyse non-functional properties such as reliability. We propose Probabilistic Component Automata (PCA) as a proba- bilistic extension to Interface Automata to automatically construct a system model by composing models of its sub-components. In par- ticular, we focus on modelling failure scenarios, failure handling and failure propagation. Additionally, we propose a novel algorithm based on Compositional Reachability Analysis to mitigate the well-known state-explosion problem associated with composable models. Both Probabilistic Component Automata and the reduction algorithm have been implemented in the LTSA tool