Model checking: towards generating a correct specification for logic controllers

Author

Weng, Xiying ; Litz, Lothar

Author_Institution

Inst. of Process Autom., Kaiserslautern Univ., Germany

Volume

6

fYear

2002

fDate

2002

Firstpage

4457

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;

fLanguage

English

Publisher

ieee

Conference_Titel

American Control Conference, 2002. Proceedings of the 2002

ISSN

0743-1619

Print_ISBN

0-7803-7298-0

Type

conf

DOI

10.1109/ACC.2002.1025352

Filename

1025352