Sciweavers

RTS
2008

Formal verification of multitasking applications based on timed automata model

13 years 3 months ago
Formal verification of multitasking applications based on timed automata model
The aim of this paper is to show, how a multitasking application running under a real-time operating system compliant with an OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several non-preemptive tasks and interrupt service routines that can be synchronized by events. A model checking tool is used to verify time and logical properties of the proposed model. Use of this methodology is demonstrated on an automated gearbox case study and the result of the worst-case response time verification is compared with the classical method based on the time-demand analysis. It is shown that the modelchecking approach provides less pessimistic results due to a more detailed model and exhaustive state-space exploration.
Libor Waszniowski, Zdenek Hanzálek
Added 28 Dec 2010
Updated 28 Dec 2010
Type Journal
Year 2008
Where RTS
Authors Libor Waszniowski, Zdenek Hanzálek
Comments (0)