Abstract FR:

Ce travail s'inscrit dans le cadre du genie automatique et traite de la specification de la partie commande de systemes automatises de production (sap). Il a pour objectif de fournir un support theorique a la definition d'outils de specification a la fois surs et faciles a utiliser. Il a ete oriente vers le grafcet dont la convivialite est attestee par sa diffusion dans les milieux de l'industrie et de l'enseignement. Cependant, il est reconnu que ce modele souffre d'ambiguites liees a son usage d'une part et a des limitations theoriques d'autre part. En particulier, le determinisme d'une realisation par grafcet depend de l'algorithme d'interpretation choisi. Nous proposons donc d'elaborer une validation du grafcet a l'aide d'une theorie des systemes sequentiels (tss) basee sur un axiome algebrique unique definissant entierement le systeme sequentiel. Par declinaisons successives de proprietes, nous construisons tout d'abord la notion de spectre, proche de celle d'automate d'etats, mais prenant en compte les specificites du grafcet (situations, receptivites, actions conditionnelles,). Nous definissons ensuite la notion de codeur qui generalise le grafcet. Cette demarche permet tout d'abord de valider les cinq regles d'evolution du grafcet, en montrant qu'elles sont indispensables a toute description de l'evolution entre les situations et donc entre les etapes. Elle donne par ailleurs une definition precise aux constituants de ce modele, ce qui permet d'exprimer formellement les conditions necessaires et suffisantes que doit respecter toute specification par grafcet. Nous demontrons ainsi que la seule erreur semantique possible est liee a la presence de boucles d'instabilite. Notre systeme formel nous permet alors de donner precisement les conditions logiques source de ces erreurs, et de les corriger automatiquement, si le specificateur le desire. Nous avons donc complete la semantique intuitive du grafcet d'une semantique mathematique, independante des realisations materielles. Ceci nous conduit a placer le grafcet au cur d'un atelier cao d'automatisme