Architecture assessment for safety critical plant operation using reachability analysis of timed automata. (July 2020)

• Record Type: Journal Article
• Authors: Gouyon, David; Pétin, Jean-François; Cochard, Thomas; Devic, Catherine
• Is Part Of: Reliability engineering & system safety. Volume 199(2020)
• Publication Date: 2020-07
• Subjects: Plant operation -- Safety assessment -- Critical process architecture -- Reachability analysis -- Timed automata -- Modelling patterns; 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.106923
• Languages: English
• ISSNs: 0951-8320

Abstract

Highlights: The challenge is to guarantee that a designed architecture can react safely. Modeling patterns help to reduce modelling time and facilitates reuse. Reachability analysis can prove the operability of architecture in some situations. Validation of the operability of generated action sequences is made by operators. Abstract: This article deals with the validation of critical industrial process architectures from the point of view of safety and operation. During the engineering phases, the objective is to complement conventional safety studies with an approach that focuses on plant operation. In this context, one of the major challenges is to provide a guarantee that the designed architecture will be able to react safely to critical situations and events. To face the complexity resulting from the large number of functionalities and devices of the installations under consideration, the proposed approach is based on dynamic models of architectures, using the formalism of timed automata and reachability analysis to verify that, given a particular configuration of an architecture, the process can be safely operated to achieve a given objective. The result is a formal tool that allows engineers and plant operators to evaluate architecture safety with different types of dysfunctional scenarios based on their operational safety expertise. The article presents the formal modelling framework, which emphasizes structured modelling using patterns to promote reuse and instantiation over several candidate architectures. The contribution is illustrated and discussed using an experimental laboratory platform.