Model checking: towards generating a correct specification for logic controllers
Xiying Weng, Lothar Litz · 2002
PLC is widely used in industrial automation systems. Due to the increasing complexity in such systems, new methods for software specifications and verifications are needed to improve the reliability of these systems. Formal methods provide promising approaches to achieve this. In this contribution, relevant criteria are proposed to get a correct specification of PLC controllers using signal interpreted Petri net (SIPN) framework. The temporal logic forms of these criteria are presented, so that model checking can be applied to verify the correctness of an SIPN design.