Formalization of Functional Block Diagrams Using HOL Theorem Proving - Abdelghany, Mohamed; Tahar, Sofiène (Anais do Simpósio Brasileiro de Métodos Formais (SBMF); 2022: Anais do XXV Simpósio Brasileiro de Métodos Formais, 2022)
Functional Block Diagrams (FBD) are commonly used as a graphical representation for safety analysis in a wide range of complex engineering applications. An FBD models the stochastic behavior and cascading dependencies of system components or subsystems. Within FBD-based safety analysis, Event Trees (ET) dependability modeling techniques are typically used to associate all possible failure/success events to each subsystem. In this paper, we propose to use higher-order logic theorem proving for the formal modeling and step-analysis of FBDs. To this end, we develop a formalization in HOL4 enabling the mathematical modeling of the graphical diagrams of FBDs and the formal analysis of subsystem-level failure/reliability. The proposed FBD formalization in HOL4 is capable of analyzing n-level subsystems with multi-state system components and enables the formal FBD probabilistic analysis for any given probabilistic distribution and failure rates.