Eventos Anais de eventos
COBEM 2023
27th International Congress of Mechanical Engineering
Model checking aided design of alarm and seal logic for ship control and monitoring system
Submission Author:
RAFAEL CELESTINO DOS SANTOS , SC
Co-Authors:
RAFAEL CELESTINO DOS SANTOS, Max Hering de Queiroz
Presenter: RAFAEL CELESTINO DOS SANTOS
doi://10.26678/ABCM.COBEM2023.COB2023-0915
Abstract
This paper presents an application of model checking (MC) to the design of Control and Monitoring System (CMS) of the Brazilian Navy (MB) Ships, with the objective of validating the safety of the specification of the alarm and seal logic implemented in Programmable Logic Controllers (PLC). The CMS is responsible for monitoring and controlling the propulsion plant and mitigating possible damage to the ship, such as fire and flooding. The alarm and seal logic aims to retain the alarm signal in the PLC until it is remotely recognized by the operator in the Human Machine Interface (HMI). The use of MC is recommended by the IEC 61508 and IEC 61511 standards for critical programmable safety systems, such as the CMS, because it is an automatic and exhaustive formal verification technique that allows validating whether the safety properties are fulfilled by the system, for all possible scenarios. A functional error in the CMS can cause a risk to the lives of the crew, material damage to the ship and environmental risks. The specification of the control logics in the MB is elaborated through Binary Logic Diagram (BLD), according to ISA 5.2. The MC aided design methodology follows these steps: 1) the safety requirements are represented by Cause and Effect Matrix (CEM), according to IEC 62881; 2) each CEM safety property is translated into two Linear Temporal Logic (LTL) formulas representing Spurious Trip Freeness (STF) and Failure on Demand Freeness (FDF), which are established by IEC 61511-1; 3) the BLD model is translated into formal Temporized Transition System (TTS), by means of the intermediary language FIACRE; 4) the LTL properties are verified in the TTS model by means of the model checker TINA/SELT. The results show that the BLD for the Alarm and Seal logic proposed by the MB design team, fulfills the FDF property, but not the STF property. Additionally, TINA/SELT presents a counterexample, from which it is possible to identify the error and to correct the BLD. After correction, a new verification has been performed. The new result shows that the corrected BLD fulfills the STF and FDF properties. In this way, the MC proves to be an efficient technique to aid engineers in identifying errors even in the early stages of the CMS design, reducing the correction costs and increasing reliability.
Keywords
Model Checking, Control and Monitoring System, programmable logic controller, Binary Logic Diagram, Cause and Effect Matrix, Linear Temporal Logic
