Formal design methodology for transforming ladder diagram to Petri nets

Ladder diagram (LD) is a common programming language at industry in order to develops control algorithms of discrete event systems. Besides, it is one of the five programming languages supported by the International Electrotechnical Commission through the IEC-61131-3 standard. Petri net (PN) theory is both a graphical and mathematical tool, which allows modeling discrete event systems in order to obtain a useful formalization to analyze them in a better way. LD control algorithms are continuously developed based on the experience of control system developers. Therefore, it is still a relevant problem on how to formalize a validation for the current and new control algorithms. In the present work, an element-to-element transformation methodology from a LD program to a PN structure is proposed. The original part of this manuscript is the proposal of five PN structures where their markings represent the states and dynamic behavior of energized and de-energized coils, which are not included in previous works. Furthermore, this methodology preserves the structural and dynamical behavior of the LD in the obtained PN. Two control algorithms of real cases are transformed using the proposed methodology.