Formal verification and implementation of real time operating system based applications

This paper presents a framework for modeling and verification of mini real-time applications running under a multitasking kernel. The model described as networks of timed automata is mapped to real time operating systemspsila tasks. We focus on cooperative scheduling tasks with different priorities. For the tasks to be as simple as possible, a unified resource access interface is necessary.