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.
Type de document :
Article dans une revue
European Journal of Automation, Hermés Science, 1997, 31 (3), pp.581--603
Liste complète des métadonnées
Contributeur : Franck Cassez <>
Soumis le : mardi 17 mars 2009 - 01:45:05
Dernière modification le : jeudi 15 mars 2018 - 14:28:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 23:32:09


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers