Formal semantics for reactive Grafcet

Franck Cassez*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)581-603
Number of pages23
JournalJournal Europeen des Systemes Automatises
Issue number3
Publication statusPublished - 1997
Externally publishedYes


  • Grafcet
  • Reactive languages
  • Sémantics
  • Timed automaton


Dive into the research topics of 'Formal semantics for reactive Grafcet'. Together they form a unique fingerprint.

Cite this