Increasing the efficiency of PLC Program Verification using a plant model

More extensive work on formal methods is now available for checking PLC (Programmable Logic Controller) programs. Some approaches propose taking into account just the control system model, while others include a plant model as well. Accordingly, the level of detail of the model is very different from one approach to the next. In this paper, we explore the contribution of such a plant model within the context of formal verification by means of Symbolic Model- Checking. Our study is primarily experimental in nature and based on a case study. A set of properties to be checked and a detailed plant model are both proposed. We then analyze how a Symbolic Model-Checking tool (the NuSMV has been selected) ensures verification of these properties either with or without a plant model.