Formal Modeling of Sequential Function Charts With Time Petri Nets

Author

Wightkin, Nicholas ; Buy, Ugo ; Darabi, Houshang

Author_Institution

Dept. of Comput. Sci., Univ. of Illinois at Chicago, Chicago, IL, USA

Volume

19

Issue

2

fYear

2011

fDate

3/1/2011 12:00:00 AM

Firstpage

455

Lastpage

464

Abstract

Sequential function charts (SFCs) are among the standard languages for programmable logic controllers (PLCs) ubiquitous in automated manufacturing and production systems. While SFCs are quite user friendly to developers, it is not easy to guarantee the correctness of safety-critical SFC programs. Thus, methods and tools for verifying the correctness of SFC programs are highly desirable. Here we introduce a transformation technique that converts a significant subset of an SFC to a time Petri net (TPN). Thanks to a large body of literature and mature tools that can analyze TPNs, our technique will bridge the gap between a user-friendly manufacturing control programming tool, the SFC, and powerful analysis tools for TPNs.

Keywords

Petri nets; factory automation; human computer interaction; program verification; programmable controllers; safety-critical software; set theory; automated manufacturing systems; automated production systems; formal modeling; programmable logic controller; safety-critical SFC programs; sequential function charts; time Petri nets; user friendly manufacturing control programming tool;

fLanguage

English

Journal_Title

Control Systems Technology, IEEE Transactions on

Publisher

ieee

ISSN

1063-6536

Type

jour

DOI

10.1109/TCST.2010.2047106

Filename

5463024