System Theoretic Model Checking for Safety Management in Industrial Plants

In recent years, the complexity of systems has increased significantly, leading to an increase in the potential for accidents or incidents in industrial plants. Therefore, such advancements and causes of accidents are frequently beyond the detection capabilities of standard safety assessment models. Traditional models define safety as managing failures and taking only direct causality into account, whereas System-Theoretic Accident Modelling and Process (STAMP) considers the causality of the accidents. STAMP is based on systems theory, in that, a STAMP system is a control system, and that control system enforces safety constraints. However, applying STAMP alone may not guarantee the correctness of the system's behavior. In this paper, the research proposes the STAMP model and Model Checking for the safety analysis of a complex socio-technical industrial system. The STAMP model identifies potential hazards and analyzes their causes and consequences. Then model checking technique is applied to verify the correctness of the system's behavior under different scenarios. In particular, the model checker technique has been used to evaluate the system's behavior against specifications, ensuring no unsafe or inappropriate behaviors. Integrating both methodologies ensure the identification of safety violations by the system giving room for improvement in system design to handle hazards and satisfy all the safety constraints identified by STAMP. On this premise, the manuscript has been grounded in the Oil & Gas sector, specifically in the Natural Gas Storage process. This approach provides a systematic way to identify hazards and verify the system’s behavior’s correctness, ultimately improving the system’s safety.