Input language | Output formal model | Source | Remarks |
IL (IEC 61131-3), ST (IEC 61131-3) | Timed Net Condition/ Event System, Petri Net, Timed automaton, SIGNAL equations, Model-checker language (SMV) | [53] - [58] | Most of the transformations are performed for verification purposes. The selected references consider the cyclic behavior of industrial controllers such as PLC for the execution of IL programs. |
LD (IEC 61131-3) | Time Petri Net, Model-checker language (UPPAAL automata) | [59] - [61] | Most of the transformations are performed for verification purposes. The selected references consider the cyclic behavior of industrial controllers such as PLC. [61] even considers multitask systems. |
FBD (IEC 61131-3), CFC, IEC 61499 | SIGNAL equations, Esterel, Interface automata, Model-checker language (UPPAAL automata, SMV) | [50] [57] [62] - [66] | Most of the transformations are performed for verification purposes. The selected references consider the cyclic behavior of industrial controllers such as PLC. [66] presents a modeling of each block by an interface automaton, the focus is placed on the IO relations: this approach could be adapted to testing of sub-components where only the IOs can be observed (black-box testing). |
SFC (IEC 61131-3) | Timed automata, Model-checker language (SMV) | [67] - [70] | SFC (61131-3) is a graphical language with hierarchical relations used to represent mainly sequential behaviors. The semantics defined in the standard contain ambiguity. An improved semantics is proposed in [70] . |
GRAFCET (IEC 60848) | Monolithic automaton, Mealy machine, Petri Net | [71] - [75] | Grafcet (60848) and SFC (61131-3) share similarities: SFC has been defined from Grafcet. The main difficulty with Grafcet is the stability research. The method presented in [71] - [73] is dedicated to black-box testing and stresses on logic input/output relations. |
Matlab Stateflow | Structural operational semantics, Continuous- Time Markov Chains | [76] [77] | The main issue with Matlab State flow models is the interpretation of junction symbols. Depending on the guards before and after a junction symbol, some transitions can be partially fired and their associated actions be executed; if no destination state can be reached after a junction, previous transitions are then backtracked to return to the previous active state without undoing the associated actions. |