Automatic verification of event-driven control programs: A case study

Execution environment and temporal performance are very important for modeling a real PLC system. They also become two impediments when verifying with model checking. This paper presents a methodology for modeling a PLC system including time and environment. In order to take into account interaction of PLC controller with execution environment, the proposed method extends the modeling method with an event-driven mechanism. The heterogeneous environments are abstracted as concurrent entities and further formalized into state graphs. A timed abstraction method is proposed to deal with real-time features which specified as timer on delay (TON). We have validated our approach on a concrete case study, a controller for steel plate transfer devices, and report on the results obtained for this case study.