The grafcet model: Discussion and integration in a multiformalism synchronous platform

Description

From modeling to validation, the synchronous approch is well-suited to design reactive real-time computer-based systems. On the other hand, in the field of production system, the graphical and synchronous model GRAFCET is widely used. However, compared to GRAFCET, synchronous languages are endowed with a more formal semantics. In order to make the best of both approches, we advocate integrating GRAFCET and synchronous languages into a common platform. This is the main objective of this thesis.First, we revisite the GRAFCET model and we give it a new semantics consistent with those of synchronous languages. The new model in named ``S-GRAFCET'' (for Synchonous GRAFCET).We then, turn to compilation problems. Two methods are introduced : the first one is a systematic rewriting of S-GRAFCET into ESTEREL programs; the second is a direct implementation of the formal semantics given to S-GRAFCET. Both compilers are operational. They are inputs to the synchronous software environment (code generators, simulators, model checkers). The full control of the compilation line allows generation of additional code that makes the verification process easier and more adequate to the application domains. The GRAFCET model itself can be used as a language for expressing properties.

Abstract (French)

De la modélisation à la validation, l'approche synchrone est bien adaptée pour concevoir les systèmes informatiques réactifs temps-réels. En Automatique, le modèle synchrone GRAFCET est largement adopté dans le milieu industriel pour modéliser les systèmes automatisés de production. Son pouvoir conceptuel est cependant limité par sa sémantique qui manque encore de formalisation. Pour bénéficier des avantages respectifs de chaque formalisme synchrone, nous péconisons une approche multiformalisme de conception. Le travail présenté dans cette thèse, vise donc à intégrer le modèle GRAFCET dans une plate-forme synchrone. Nous souhaitons ainsi rapprocher les domaines de l'Informatique et de l'Automatique.Pour celà, nous sommes d'abord revenu sur les problèmes d'évolution et de définition qui se rattachent à la sémantique du GRAFCET. Cette étude nous a conduit à définir un nouveau modèle : S-GRAFCET fondé sur une nouvelle interprétation des règles d'évolution.Nous nous sommes ensuite intéressé à la compilation du S-GRAFCET. Deux méthodes sont présentées dans le mémoire, elles ont permis l'élaboration de compilateurs opérationnels. La première est basée sur une réécriture systématique des comportements en ESTEREL, la seconde sur la recherche directe des états stables. Le code généré (machine à états finie) est le point d'entrée pour des générateurs, des simulateurs et des outils de preuves propres à l'approche synchrone. La maîtrise complète de la chaîne de compilation permet également de réaliser des vérifications plus proches du domaine d'application et d'exprimer les propriétés de sûreté en systèmes d'équations booléennes ou directement en GRAFCET.

Additional details