Abstract : 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 equipping GRAFCET with a formal semantics to obtain a behavioural model (namely a timed automaton) that captures the metric aspect of time.
https://hal.inria.fr/inria-00368571 Contributor : Franck CassezConnect in order to contact the contributor Submitted on : Tuesday, March 17, 2009 - 1:45:05 AM Last modification on : Wednesday, April 27, 2022 - 3:50:42 AM Long-term archiving on: : Tuesday, June 8, 2010 - 11:32:09 PM