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.