Verification of IEC61131-3 based safety applications is a challenge in the development process of industrial systems. In this paper, we formally describe a set of transformation rules we have defined for the automatic transformation of IEC61131-3 function block based safety applications to UPPAAL timed automata models. These models are next used for the verification process of the safety application. Both the source and the target domain models have been formally defined and these definitions are used for the formal definition of the transformation rules. We adopted as format of the source models the PLCopen XML specification that is widely accepted by industry. Based on this format and the defined transformation rules a prototype model transformer was developed using Java. The transformer was used on several safety applications to verify its functionality and the effectiveness of the transformation process. |
