Analyse de Grafcets par Génération Logique de l'Automate Équivalent
Roussel, Jean-Marc · HAL (Le Centre pour la Communication Scientifique Directe) · 1994
In Automation Engineering, GRAFCET is currently used for modelling sequential system control, for its modeling and ergonomic capacities. It has nevertheless been reproached with not being defined formally enough for all established grafcets to be unequivocal and validated. The aim of this work is twofold: to contribute to the formalization of GRAFCET so as to strengthen its theoretical foundations and to provide all analysts with the necessary means to validate GRAFCET models by proving their properties and their behavior in relation with inputs/outputs. As GRAFCET is a complex state machine - essentially because of the important parallelisms the description of which it allows - the analyst can use the graph of accessible situations to validate his specification. We have conceived a technique to automatically generate the graph of accessible situations of a global grafcet (i.e the equivalent finite state machine) so as to establish a set of proofs and properties about the inner coherence of the grafcet and its relevance in relation to requirements. A Boolean algebra in which the notion of events has been formalized by two unary operations has been built. The 14 properties that have been demonstrated have allowed to establish a module of formal calculus used to review the evolution of inputs.Our works include extensions of GRAFCET models. To validate our approach, a C software has been developed which is used to calculate the finite state machine equivalent to the grafcet to be validated. To check certain properties, we use the MEC software which has been developed to study transition systems. Two examples of validations of gafcets by analysis of their automate are given in the paper.