Framework para Aplicação de Model Checking ao Projeto de Automação no Ambiente Industrial

Abstract

This paper proposes a framework for applying model checking in industrial control design based on the GRAFCET language. The aim of this research was to develop a step- by-step to help create a digital twin with a cyberphysical aspect of a system composed of a control program and a plant to be controlled. For this, it is proposed, through manual inspection, the creation of templates of the most common modules that compose the internal and external environment of the control. The creation of models in state machine was used for the environments and for the control itself. The application of model checking is done through the NuSMV tool, which has its own language based on state evolution with property verification in Computation Tree Logic - CTL. For illustration purposes, a example of a valve with all the components found in more recent real projects in the oil and gas industry is introduced. The result was a model capable of experimenting with execution paths and analyzing them by verifying the security and operating properties of the system. Additionally, a validation of the initially designed control program was successfully carried out, being able to serve, in a real application, as a complement to a factory acceptance test before its implementation in an embedded PLC.