In order to apply the techniques of model checking to verify an LD (Ladder Diagram) program using the available tools, it is necessary to represent the semantics of the program in formal language. The semantic transformation is based on the metamodel of the Ladder Diagram language and metamodel of the TPN (Time Petri Nets). It was coded using ATL (ATLAS Transformation Language). These elements have a unique semantics so a complete translation would have to take into account the specific semantic of each function block (FB).
The ATL code is composed in eight matched rules. A match rule enables to match some of the model elements of a source model, and to generate a number of distinct target model elements. We use inheritance rule to filter different elements that are represented by a unique class in the metamodel. This inheritance had been done at the metamodel level but our approach allows keeping the metamodel at higher abstraction level and allows to factorize the ATL code.
Each Ladder Diagram program will be translated to a TPN. This TPN can be divided in three different groups of elements, each one with a different purpose during the simulation.
The first group is responsible to control the execution according to the PLC operation, a place is introduced for each execution step, read the inputs, execute all the ordered rungs one by one, then update the outputs.
The second group represents the variables value. Each variable contained in the program will be translated into two places, one representing the True (VariableName_1) and the other the False (VariableName_0) state of the variable.
The third group represents the semantics execution, this group is composed two places for each variable as in the second group. But in this case the variables do not represent the real value variable, but are used to calculate the new values.