Formal Verification of Safety Analysis Models of Repairable and Reconfigurable Systems
Elodie Kobeissi, Pierre-Yves Piriou, Jean-Marc Faure · IFAC-PapersOnLine · 2017
This paper proposes a method to formally check whether formal properties hold on a dynamic model which has been designed by experts for Model Based Safety Analysis/Assessment. As repairable and reconfigurable systems are considered, this model is assumed to be described in the Generalized Boolean-logic Driven Markov Processes (GBDMP) modelling framework. Translation rules are given to obtain a formal model that describes correctly the evolution of the initial model with the semantics of the verification tool. The approach is exemplified on a simple case of standby redundancy.