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 language | English |
|---|---|
| Pages (from-to) | 581-603 |
| Number of pages | 23 |
| Journal | Journal Europeen des Systemes Automatises |
| Volume | 31 |
| Issue number | 3 |
| Publication status | Published - 1997 |
| Externally published | Yes |
Keywords
- Grafcet
- Reactive languages
- Sémantics
- Timed automaton