Analysis of Real Time Operating System Based Applications

This text is dedicated to modelling of real-time applications running under multitasking operating system. Theoretical background is based on timed automata by Alur and Dill. As this approach is not suited for modelling preemption we focus on cooperative scheduling. In the addition, interrupt service routines are considered, and their enabling/disabling is controlled by interrupt server considering the specified server capacity. The server capacity has influence on the margins of the computation times in the application processes. Such systems, used in practical real-time applications, can be modelled by timed automata and further verified since their reachability problem and model checking of TCTL problem is decidable. Use of this methodology is demonstrated on the case study.

• Type: Conference
• Year: 2003
• Where: FORMATS
• Authors: Libor Waszniowski, Zdenek Hanzálek
• Keywords: FORMATS 2003, Real-time Applications, Server Capacity, Timed Automata