Résumé : Les étapes de rédaction du cahier des charges et de spécification sont cruciales pour la sureté de fonctionnement des systèmes automatises de production. Dans ce cadre, nous proposons une méthode permettant de couvrir les phases allant de la vérification du cahier des charges a la validation des spécifications. En particulier, l'approche que nous proposons pour la vérification et la validation formelles de spécifications de systèmes logiques à évènements discrets repose sur une formalisation algébrique du cahier des charges et du Grafcet de spécification. Nous utilisons un modèle algébrique base sur les corps finis (ou de Galois) d'ordre 2 et une modélisation du temps continu a dates discrètes. La combinaison de ces deux modélisations forme un modèle algébrique temporel (la théorie du signal hyperfini ou TSH) propre à représenter les systèmes logiques à événements discrets. La vérification du cahier des charges exprime en langage naturel commence par une étape d'expression du cahier des charges en logique temporelle PCTL#*, suivie d'une traduction de cette formulation en équations différentielles en TSH. Elle se termine par la détection a partir de cette expression algébrique d'éventuelles incohérences ou redondances du cahier des charges. Nous proposons une méthode de vérification formelle de Grafcets en 5 étapes : vérification syntaxique du Grafcet, écriture du Grafcet de spécification en équations différentielles en TSH, d2duction de propriétés dynamiques de la structure du Grafcet, simplification des équations d'évolution du Grafcet de spécification à partir de ces propriétés, vérification des équations représentant le Grafcet de spécification. Enfin, pour valider le Grafcet, nous utilisons les représentations du cahier des charges et des évolutions du Grafcet sous forme d'équations différentielles en TSH et validons les spécifications en Grafcet par comparaison des équations du Grafcet et de celles du cahier des charges. Nous concluons sur les applications et perspectives de la méthode.
Notes : Bibliogr. p. 227-241. Annexes
Thèse de doctorat : Sciences Appliquées : Ecole Normale Supérieure de Cachan : 1997 (version d'origine)