Formal Modeling of Sequential Function Charts With Time Petri Nets

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.