Formal verification and implementation of real time operating system based applications
Tudor Zaharia, Piroska Haller · 2008
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 systems’ 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.