Modeling, Verification, and Implementation of PLC Program using Timed-MPSG
Devinder Thapa, Sang Chal Park, Chang Mok Park and Gi-Nam Wang
Summer Computer Simulation Conference 2007 (SCSC 2007)
San Diego, California (USA), July 15-18, 2007
Abstract
Abstract— In this paper, we proposed a methodology to model, verify, and generate IEC standard PLC code using Timed-MPSG (an extended version of finite state automata). Firstly, this state machine is use to model the formal specification of the process, after that, the textual structure of Timed-MPSG translated to input code for model checker (SMV), for the purpose of formal verification. And finally, generation of programmable logic controller code by one-to-one mapping technique. The similarity in the hierarchical structure of Timed-MPSG and IEC standard has made it convenient to transform from one form to another. Although, the simulation can be used to verify the written code, however, the use of formal methods for verification is more desirable to validate the state model for hidden errors. Furthermore, an illustration of methodology to PLC design and development is explained with a suitable example.