A tool, coded in Haskell, to translate the XML representation of Sequential Function Chart See PLCOpen, which is generated by the PLC IDE Beremiz, to its corresponding KeYmaera hybrid program.
This tool is a result of my MSc dissertation entitled "Validation of IEC 61131-3 Programmable Logical Controllers in KeYmaera". The main goal of the dissertation is to use KeYmaera as a tool to validate safety proprieties about a PLC program. This dissertations focused on the SFC language and the overall process of how to convert SFC to a hybrid program.
The figure illustrates how the tool actually works,
-
It begins by parsing the XML given by Beremiz and stores the result in a structure called SFC HXT. This first part was made with the HXT library to parse and input file, hence the name of the structure.
-
The next step in the diagram is the translation of the SFC HXT to the SFC+ formal, the "+" is introduced by the dissertation to upgrade the language and make the annotation of the dynamics of the system possible, and consequently the annotation of other details.
-
The third step is to translate the SFC+ formal to hybrid automaton which was possible by the hybrid sequential function charts .
-
The final step is possible since hybrid automaton can be directly represented in hybrid program. (see example here).
Please if you detect any bug or incoherence in the program feel free to make a pull request!
Firstly, you will have to code a SFC program in Beremiz IDE and annotate it. Note that the SFC that is accepted by the tool in merely a subset of the language, namely:
- The types accepted by the tool are: INTEGER, REAL and BOOLEAN the others will be ignored;
- The only type of variables stored are the input, local and output variables;
- The step actions are coded in ST assignments;
- The conditions of the transtition are coded in ST conditions;
There are 5 types of annotations:
- CODE annotation: Where the dynamics of the step are annotated e.g "@step->ODE1:Cond1;ODE2,ODE2.1:Cond2\n@step1->ODE11:Cond11"
- initAnnotation: Where the precondition of the program is presented e.g "@initCond:Cond".
- invariantAnnotation: Where the invariant of the program is presented e.g "@invariant:Cond".
- toProveAnnotation: Where the prostcondition of the program is presented e.g "@toProveCond:Cond".
- ExtrasAnnotation: The condition which once the program is translated it is not useful for the hybrid program is then traded by one that is actually useful. e.g "@Extras:\nCondToReplace:NewCond\n".
Then, having the Haskell platform installed, in the terminal type:
runhaskell parserSFC.hs srcsrc is the path of the XML file with the SFC code. The generated .key file will be in the same directory of the parserSFC file.