Title :
Model checking: towards generating a correct specification for logic controllers
Author :
Weng, Xiying ; Litz, Lothar
Author_Institution :
Inst. of Process Autom., Kaiserslautern Univ., Germany
Abstract :
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.
Keywords :
Petri nets; formal specification; process control; program verification; programmable controllers; temporal logic; PLC; formal methods; industrial automation; model checking; programmable logic controllers; reliability; signal interpreted Petri net; software specification; software verification; temporal logic; Automatic control; Automatic generation control; Automation; Concurrent computing; Electrical equipment industry; Logic design; Power system modeling; Process control; Programmable control; Signal processing;
Conference_Titel :
American Control Conference, 2002. Proceedings of the 2002
Print_ISBN :
0-7803-7298-0
DOI :
10.1109/ACC.2002.1025352
