02 Jul 2019 - Dan Kristiansen
The overall goal of this project is to design and implement a compiler that can improve quality and efficiency of PLC-systems, by translating IEC 61131-3 languages into an equivalent timed formal model.
The formal model can then be a very powerful tool to represent the timing of sub-parts of the program, and even the entire control flow. Existing model checker tools allow such models to be verified with respect to specifications. It can for example check whether a deadlock can occur and whether certain parts of the model is reachable.
We propose an Intermediate Representation(IR) language and define its syntactic structures. Essentially, a program in the \gls{IR} is a set of simple commands, where each command has a unique label and explicitly states where the control flow should proceed after executing the command.
The translation rules from IR to TAPN create an abstraction from the information in IR,to model nondeterministic choices in if,case, and loop. It is worth noticing, that the translations only consider the timing and control flow of the statements, hence the values of the variables are disregarded.
A call statement, shown above, creates an intermediate place lx’, that holds the current position in the control flow, while the called action or function is executed. When a token is produced in special label slend, the next transition in the flow is enabled and the control flow proceed to place ly.
The language and the translations rules are defined in the programming language Haskell.
The picture below shows a computed Petri Net representation of a PLC program.
