Abstract FR:

La commande de nombreux systemes automatises est programmee en grafcet. Dans ce langage metier de l'automatisation, le temps joue un role important pour le controle de ces systemes. Comme le temps apparait egalement dans les proprietes critiques que doivent satisfaire certaines applications, nous nous sommes interesses a la verification temporelle de grafcet. Tout d'abord nous avons essaye d'introduire le temps dans les modelidations qui avaient deja ete donnees pour le grafcet au sein de l'equipe : le langage signal et les systemes de transitions. L'hypothese suivante a alors ete faite : un pas de cycle dans le cas de signal, le franchissement d'une transition dans celui des systemes de transitions representent une unite de temps. Ceci nous a permis de verifier des proprietes temporelles lorsque le grafcet considere ne comportait pas plus de deux temporisations avec des delais brefs. En effet cette modelisation du temps conduit a une croissance exponentielle du nombre d'etats rendant tres vite les verifications impossibles. Pour resoudre ce probleme, nous nous sommes tournes vers des formalismes qui des leur definition prennent en compte le temps physique. Nous avons ainsi modelise le grafcet grace aux automates temporises, exprime les proprietes en logique tctl et utilise l'outil de verification kronos. Grace a cette methode, nous avons pu verifier des proprietes sur des grafcets comportant davantage de temporisations ayant eventuellement de grands delais. Cependant la taille des automates demeure une limite pour nos verifications. Nous avons envisage differentes solutions : prendre en compte l'environnement pour reduire la taille de l'automate, utiliser des techniques de verification, proposer une modelisation plus condensee en automate temporise. Elles nous ont permis d'etendre le champs des grafcets verifiables. Ces methodes ont ete appliquees a differents procedes dont la cellule de production korso.