Grafcet revisited with a synchronous data-flow language

The Grafcet (or sequential function charts) language is a graphic language often offered in programmable logic control systems (PLC) used for industrial control-command applications. Modeling of Grafcet by the synchronous data-flow language Signal gives both explicit semantics, and the corresponding simulator. The translation into a graph of tasks makes it possible to execute the Grafcet program on any hardware architecture. Moreover, the use of Signal´s proof tools allows verification of Grafcet properties, opening the field of critical applications to this very expressive language