Formal semantics for reactive Grafcet

Franck Cassez*

*Corresponding author for this work

Research output: Contribution to journalArticle

2 Citations (Scopus)

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 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
Volume31
Issue number3
Publication statusPublished - 1997
Externally publishedYes

Keywords

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

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

  • Cite this