Model checking of security systems specified by GRAFCET and Cause and Effect Matrix

Abstract

This paper presents a methodology assisted by model checking for the development of safety systems implemented in Programmable Logical Controllers based on specifications prepared in Binary Logical Diagram (BLD). In order to validate the DLB in the initial design stage, the safety requirements are represented by Cause and Effect Matrix (CEM) and sequential logics by GRAFCET. A method is proposed that systematizes all these requirements in an expanded CEM and a set of GRAFCET structural properties, from which the properties are extracted into temporal logic formulas for the MC algorithm. The proposal is elucidated by the development of the BLD for a motor start and stop logic, where the MC of properties automatically extracted from the MCE and the GRAFCET allowed the identification and correction of errors in the DLB through counterexamples until converging to a formally validated DLB.