Model Checking the Multi-Formalism Language FIGARO

This paper presents a probabilistic model-checking tool for FIGARO, a multi-formalism modelling language that includes e.g., generalised stochastic Petri nets, Boolean-logic driven Markov processes, telecommunication networks, dynamic reliability block diagrams, process diagrams, and electric circuits. FIGARO has been developed and maintained by EDF for the analysis of system dependability such as reliability, availability and maintainability. We present a probabilistic model-checking tool for FIGARO models. It combines efficient, fully automated verification algorithms with numerical analysis techniques. Whereas the existing FIGARO tools, the Monte Carlo simulator YAMS and the most-probable-sequence explorer FiGSEQ, provide respectively statistical guarantees and upper bounds for unreliability and unavailability, our tool provides hard guarantees: its results are correct up to a given numerical accuracy. The key ingredient is the tool-component FiGAROAPI that enables the state-space generation for FIGARO models thus facilitating model checking. This paper describes the details of FiGAROAPI and empirically evaluates the feasibility and merits of the proposed framework. FiGAROAPI leverages upon the state-of-the-art STORM model checker as back-end, and it can model check various types of formalism in their FIGARO representation.