D Une Theorie Des Systemes Sequentiels A La Notion De Codeur Validation Globale Du Grafcet

D'une theorie des systemes sequentiels a la notion de codeur : validation globale du GRAFCET

Du TTM/RTTL pour validation des systemes commandes par GRAFCET

Le modèle GRAFCET

De la modélisation à la validation, l'approche synchrone est bien adaptée pour concevoir les systèmes informatiques réactifs temps-réles. 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 pré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.