Verification of a Timed Multitask System With Uppaal

System and program verification has been a large area of research since the introduction of computers in industrial systems. It is an especially important issue for critical systems, where errors can cause human and financial damages. Programmable Logic Controllers (PLCs) are now widely used in many industrial systems and verification of the corresponding programs has already been studied in various contexts for a few years, for the benefit of users and system designers. First restricted to an untimed setting, verification was recently extended to systems where quantitative constraints are needed, possibly related to time elapsing. For instance, timed features like TON (Timers ON delay), used in PLC programs, were modeled with timed automata, thus increasing the size of the verification problems addressed. In this framework, we propose the modeling and verification of a particular timed multitask PLC program, which is part of the so-called MSS (Mecatronic Standard System) platform from Bosch Group. In this case study, time aspects are combined with multitask programming, which raises questions related to the reaction time between the detection of a signal and the resulting event. 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, which is first described in SFC then translated 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.