Vérification formelle de chaines de contrôle-commande d'éléments de conception standardisés
Résumé
Cet article présente la mise en œuvre de vérifications formelles sur une bibliothèque d'éléments standards utilisés pour la conception de programmes de commande et d'interfaces de supervision. L'originalité des travaux porte sur la vérification conjointe de la chaîne de contrôle-commande complète des éléments de la bibliothèque. Le programme de commande, l'interface de supervision et la partie opérative associés aux éléments sont modélisés sous forme d'automates temporisés de même que le comportement de l'utilisateur face à l'interface de supervision. Les exigences à satisfaire sont écrites en CTL, puis vérifiées par Model-Checking (UPPAAL). Nous appliquons notre approche sur les modèles d'une vanne motorisée utilisable dans un contexte industriel. Les résultats montrent l'efficacité des méthodes formelles dans la détection des erreurs de conception des programmes de commande et des interfaces de supervision.