Titre: Modélisation et vérification des aspects temporisés des langages pour automates programmables industriels
Auteurs: Mohamed El Mongi BEN GAID
Ecole : Université Paris Sud – XI
Pages : 68
Résumé : Depuis quelques années, de nombreux travaux de recherches visant à améliorer la sûreté de ces applications par les méthodes formelles ont été réalisés [FL00]. L’apport de ces méthodes a été très important. Nous nous intéressons particulièrement à la technique du model-checking [SBB+99, CGP99]. Cette technique permet de vérifier si un modèle vérifie une propriété en explorant exhaustivement tous les comportements décrits par le modèle. Le premier chapitre illustre le principe de fonctionnement des API et les langages normalisés utilisés pour leur programmation et définis dans la norme IEC 61131-3. Le deuxième chapitre décrit les différents aspects temporisés qui interviennent lors de l’exécution d’un programme sur un API.
Le troisième chapitre dresse un état de l’art des modèles prenant en compte ces aspects temporisés, et destinés à être vérifiés par model-checking. Le quatrième chapitre présente certains aspects de modélisation permettant de réduire considérablement la complexité de la vérification des propriétés temporisées. L’apport des modèles décrits est validé expérimentalement sur des exemples non triviaux.
Téléchargement du fichier PDF du rapport PFE : Modélisation et vérification des aspects temporisés des langages pour automates programmables industriels