Proposition of plant model for the verification of system safety

Previously, we define an approach that screens the dangerous evolutions to secure the manufacturing system. For that, a filter with a constraints set, is defined. Indeed, these constraints are located in a filter between the plant and the controller, to filter outputs which can damage the plant. In this paper, we propose a verification approach to ensure the sufficiency of constraints. This verification is performed by model checking that requires a system model (plant, Programmable Logic Controller evolution, and control program). This paper proposes a system model taking into account the computing environment as well as the technology of plant elements and system instrumentation. This model is proposed to make the verification of the constraints sufficiency. We propose a modular system modelling to consider each plant element separately, and considering each stage of the functional chain. The modelling tool used is timed automata because they enable to synchronise different models. An example of double-acting cylinder driven by a 5/2 air valve, illustrates this proposal.