Verification of a timed multitask system with UPPAAL

Author

Mokadem, H.B. ; Bérard, Béatrice ; Gourcuff, Vincent ; Roussel, Jean-Marc ; De Smet, Olivier

Author_Institution

LSV, CNRS UMR & ENS de Cachan

Volume

2

fYear

2005

fDate

19-22 Sept. 2005

Lastpage

354

Abstract

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

Keywords

automata theory; formal verification; multiprogramming; programmable controllers; Ladder Diagram; MSS; PLC program; UPPAAL; control program; mecatronic standard system; model checking; system designer; timed automata; timed multitask system; Automata; Automatic control; Automatic programming; Clocks; Control systems; Programmable control; Safety; Size control; Synchronization; Time factors; Model Checking; Programmable Logic Controllers; Timed Automata;

fLanguage

English

Publisher

ieee

Conference_Titel

Emerging Technologies and Factory Automation, 2005. ETFA 2005. 10th IEEE Conference on

Conference_Location

Catania

Print_ISBN

0-7803-9401-1

Type

conf

DOI

10.1109/ETFA.2005.1612699

Filename

1612699