Model Checking the Multi-Formalism Language FIGARO

IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 463–470

Abstract

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.

Authors 5

1. Shahid Ali Khan Aachen Software Modeling and Verification

   RWTH Aachen University

   Affiliation as printed

   Software modeling and verification, RWTH Aachen University, Aachen, Germany

2. Matthias Volk Aachen Software Modeling and Verification

   RWTH Aachen University

   Affiliation as printed

   Software modeling and verification, RWTH Aachen University, Aachen, Germany

3. Joost-Pieter Katoen Aachen Software Modeling and Verification

   RWTH Aachen University

   Affiliation as printed

   Software modeling and verification, RWTH Aachen University, Aachen, Germany

4. Alexis Braibant

   Électricité de France (France)

   Affiliation as printed

   R & D/PERICLES department, Électricité de France, Palaiseau, France

5. Marc Bouissou

   Électricité de France (France)

   Affiliation as printed

   R & D/PERICLES department, Électricité de France, Palaiseau, France