Statistical model checking of stochastic component-based systems

ABSTRACTBehaviour-interaction-priority (BIP) is a component-based framework that supports the rigorous design of embedded systems. This paper discusses stochastic BIP (SBIP) component systems, which involve semantics-based Markov chain models. We develop a method to translate the systems from SBIP into the models specified in the PRISM language. A bisimulation minimization approach is proposed to overcome the problem of state-space explosion of model checking. Finally, to illustrate the effectiveness of the proposed methods, we discuss a case study involving clock synchronization protocols for statistical and probabilistic model checking.