Model Checking of Multitasking Real-Time Applications Based on the Timed Automata Model Using One Clock

The aim of this chapter is to show how a multitasking real-time application running under a real-time operating system can be modeled by timed automata. The application under consideration consists of several preemptive tasks and interrupts service routines that can be synchronized by events and can share resources. A real-time operating system compliant with an OSEK/VDX standard is considered for demonstration. A model checking tool UPPAAL is used to verify time and logical properties of the proposed model. Since the complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.