Journal of Applied Mathematics
Volume 2013 (2013), Article ID 721624, 9 pages
http://dx.doi.org/10.1155/2013/721624
Research Article

Component-Based Formal Modeling of PLC Systems

Rui Wang,1,2 Yong Guan,1,2 Luo Liming,1 Xiaojuan Li,1,2 and Jie Zhang3

1College of Information Engineering, Capital Normal University, Beijing 100048, China
2National Lab for ISAT, Beijing 100048, China
3College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China

Received 8 February 2013; Accepted 27 February 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Rui Wang et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

Abstract

Functional validation is an important task in complex embedded system. The formal modeling of PLC system for verification is a rough task. Good verification model should be faithful and concise. At one hand, the model must be consistent with the system at the other hand, the model must have suitable scale because of the state explosion problem of verification. This paper proposes a systemic method for the construction of verification model. PLC system architecture and PLC features are modeled as components. This is universal for all PLC applications. We give an automatic translation method for software modeling based on operational semantics. A small example is demonstrated for our approach.