| Titre |
Formal Modeling of Grafcets With Time Petri Nets |
| Auteurs |
SOGBOHOSSOU MEDESU [1],
VIANOU Antoine [2],
|
| Journal: |
IEEE Transactions on Control Systems Technology |
| Catégorie Journal: |
Internationale |
| Impact factor: |
3.882 |
| Volume Journal: |
23 |
| DOI: |
10.1109/TCST.2015.2388491 |
| Resume |
Grafcet standard (IEC60848) is a formalism used in the world of manufacturing control, at the behavioral specification stage of a system. For specifying safe-critical systems, mathematical models associated with model-checking tools are necessary for the validation of the correctness. However, grafcets (meaning grafcet diagrams) are only semiformal models since certain aspects may be a source of different interpretations. The usual practice is to go through an intermediate formalism. In this brief, time Petri nets (TPNs) are chosen because they combine simplicity with wide-spreading and they also allow quantitative time analyses useful for the verification of real-time specifications. The main goal is to propose a principle of transforming a grafcet into TPN and to define the rules of this translation. The obstacle to overcome is to conciliate synchronous semantics of grafcet with asynchronous semantics of TPN. |
| Mots clés |
time Petri nets (TPNs), Grafcet, inhibitor arcs, read arcs, synchronous hypothesis |
| Pages |
1978 - 1985 |
| Fichier |
|