Formal semantics for reactive Grafcet

Grafcet is a graphical formalism derived from Petri Nets and widely used to program automation applications. So far, this formalism has not been equipped with a formal semantics : interpretation algorithms give the meaning of a Grafcet description. Our purpose is to take advantage of the work carried out for reactive languages : these languages are given a precise behavioural semantics by means of finite-state machines ; the behavioural model can then be checked for various properties. The work presented hereafter consists in equiping Grafcet with a formal semantics to obtain a behavioural model (namely a timed automaton) that captures the metric aspect of time.