Date
2005
Indexation documentaire
Informatique générale
Subject
Programmable Logic Controllers; Timed Automata; Model Checking
Titre du colloque
10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2005)
Date du colloque
09-2005
Ville du colloque
Catane
Pays du colloque
Italie
Titre de l'ouvrage
Proceedings of 10th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2005, September 19-22, 2006, Catania, Italy
Nom de l'éditeur
IEEE
Année
2005
ISBN
0-7803-9401-1
Auteur
Roussel, Jean-Marc
De Smet, Olivier
Bel Mokadem, Houda
Bérard, Béatrice
Gourcuff, Vincent
Type
Communication / Conférence
Résumé en anglais
Since it is an important issue for users and system designers, verification of PLC programs has already been studied in various contexts, mostly for untimed programs. More recently, timed features were introduced and modeled with timed automata. In this case study, we consider a part of the so-called MSS (mecatronic standard system) platform from Bosh group, a framework where time aspects are combined with multitask programming. Our model for station 2 of the MSS platform is a network of timed automata, including automata for the operative part and for the control program, written in Ladder Diagram. This model is constrained with atomicity hypotheses concerning program execution and model checking of a reaction time property is performed with the tool UPPAAL.
