Abstract (FR)

Dans ce travail, nous nous intéressons aux aspects temporisés de la programmation des automates programmables industriels (API). La vérification des programmes d'API est un enjeu important pour les constructeurs, ce qui a déjà suscité de nombreux travaux. L'étude de propriétés quantitatives faisant intervenir le temps a été abordée plus récemment, avec des difficultés supplémentaires liées à l'introduction de temporisateurs et d'horloges. En utilisant l'exemple d'un mécanisme d'évaporation, nous proposons une modélisation du système contrôlé ainsi que du programme de contrôle écrit en Ladder Diagram, sous la forme d'un réseau d'automates temporisés, avec une hypothèse forte d'atomicité pour l'ensemble des instructions du programme. Nous montrons, sur cet exemple, comment cette hypothèse permet de réduire la taille du modèle et d'accélérer les calculs d'accessibilité. Les performances sont illustrées par la vérification de plusieurs propriétés de l'évaporateur avec l'outil Uppaal.