Verification of an evaporator system with Uppaal

Ben Gaid, Mongi; Bérard, Béatrice; de Smet, Olivier

Ben Gaid, Mongi; Bérard, Béatrice; de Smet, Olivier (2005), Verification of an evaporator system with Uppaal, Journal Européen des Systèmes Automatisés, 39, 9-10, p. 1079-1098. http://dx.doi.org/10.3166/jesa.39.1079-1098

Type

Article accepté pour publication ou publié

Date

2005

Journal name

Journal Européen des Systèmes Automatisés

Volume

Number

9-10

Publisher

Hermès

Pages

1079-1098

Abstract (FR)

Dans ce travail, nous nous intéressons à des aspects temporisés de la programmation des automates programmables industriels (API). 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, avec l'outil UPPAAL, comment cette hypothèse permet d'améliorer les performances pour la vérification de propriétés de ce système.

Abstract (EN)

In this work, we study some timed features for PLC (Programmable Logic Controller) programming. This study is illustrated with a two tanks system for which we propose a component based model. The control program, written in Ladder Diagram, as well as the operating part are modeled by a network of timed automata, with a strong hypothesis of atomicity about program execution. We show on this example, using the tool UPPAAL, how this hypothesis increases the efficiency of verification for several properties of the system.

Subjects / Keywords

Automates programmables industriels; Automates temporisés; Model checking