Skip to Main content Skip to Navigation
Journal articles

Formal Semantics for Reactive {GRAFCET}

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Franck Cassez <>
Submitted on : Tuesday, March 17, 2009 - 1:45:05 AM
Last modification on : Wednesday, December 19, 2018 - 3:02:04 PM
Long-term archiving on: : Tuesday, June 8, 2010 - 11:32:09 PM


Files produced by the author(s)


  • HAL Id : inria-00368571, version 1


Franck Cassez. Formal Semantics for Reactive {GRAFCET}. European Journal of Automation, Hermés Science, 1997, 31 (3), pp.581--603. ⟨inria-00368571⟩



Record views


Files downloads