Formalization of Functional Block Diagrams Using HOL Theorem Proving

• Mohamed Abdelghany Concordia University
• Sofiène Tahar Concordia University

Resumo

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.

Palavras-chave: Functional block diagrams, Event trees, Safety analysis, Higher-order logic, Theorem proving, HOL4