Un cadre pour la vérification automatique de programmes IL

Nous nous intéressons à la vérification automatique de programmes d'API (automates programmables industriels) écrit dans le langage IL (Instruction List), un des cinq langages définis par la norme IEC 61131-3. Nous proposons une sémantique formelle d'un sous-ensemble représentatif du langage IL et un codage direct de cette sémantique dans un outil de model-cheking. Nous vérifions ensuite automatiquement des propriétés comportementales riches exprimées dans une logique temporelle linéaire. La pertinence de notre approche est illustrée par le traitement de l'exemple d'un chariot automoteur sur rail.