Formalism and semantics of PyCATSHOO: A simulator of distributed stochastic hybrid automata. (April 2021)

• Record Type: Journal Article
• Authors: Desgeorges, Loïc; Piriou, Pierre-Yves; Lemattre, Thibault; Chraibi, Hassane
• Is Part Of: Reliability engineering & system safety. Volume 208(2021)
• Publication Date: 2021-04
• Subjects: Stochastic hybrid automata -- Formalization -- Semantics -- Inference rules -- Model based safety analysis -- Simulation; Reliability (Engineering) -- Periodicals; System safety -- Periodicals; Industrial safety -- Periodicals; Fiabilité -- Périodiques; Sécurité des systèmes -- Périodiques; Sécurité du travail -- Périodiques; 620.00452
• DOI: 10.1016/j.ress.2020.107384
• Languages: English
• ISSNs: 0951-8320

Abstract

Abstract: This article lays the mathematical foundations of PyCATSHOO, a Model-Based Safety Analysis (MBSA) framework relying on distributed stochastic hybrid automata. This tool was initially developed for use cases where continuous evolution of physical variables or component failure rates matter to assess the dependability attributes. The modelling language has been designed in order to provide to the analyst the best expressiveness and ease of use. Nevertheless, although the structure and behaviour of a PyCATSHOO model have been informally described previously, they have never been formally established, which precludes its scientific acceptance and slows down its adoption by new users. To fill this lack, this article introduces formal definitions of the structure of PyCATSHOO models using set theory and of their operational semantics using inference rules (exactly 1 axiom and eight inference rules). These formal definitions are illustrated on a simple case study: the heated room. As a result, our proposing disambiguates the semantics of PyCATSHOO models, provides a formal specification of its input language and the core logic of its simulator engine and paves the way to the integration of model checking techniques in the PyCATSHOO framework. Highlights: This paper refines the modelling formalism of PyCATSHOO, a Model-Based Safety Analysis framework. It proposes a formalization of its semantics using inference rules. This formalization paves the way to the formal verification of PyCATSHOO models through model-checking techniques.