A Formally Verified Application-Level Framework for Real-Time Scheduling on POSIX Real-Time Operating Systems
Issue No. 09 - September (2004 vol. 30)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2004.45
Peng Li , IEEE
Binoy Ravindran , IEEE
Syed Suhaib , IEEE
This paper presents a framework, called meta scheduler, for implementing real-time scheduling algorithms. The meta scheduler is a portable middleware layer component designed for implementations over POSIX-compliant operating systems. It accommodates pluggable real-time scheduling algorithms while offering the flexibility of platform independence—the singular underlying OS requirement is the now nearly ubiquitous POSIX compliance. The versatility of pluggable schedulers positions the meta scheduler for deployment in an interoperable heterogeneous real-time environment. We present the design of the meta scheduler and outline its implementation. Furthermore, we present a mechanized correctness verification using the UPPAAL model checker. Prototype implementation of the meta scheduler over QNX Neutrino real-time operating system demonstrates high performance and a small footprint.
Real-time scheduling, time/utility functions, utility accrual scheduling, Portable Operating System Interface (POSIX), model checking.
Peng Li, Binoy Ravindran, Syed Suhaib, Shahrooz Feizabadi, "A Formally Verified Application-Level Framework for Real-Time Scheduling on POSIX Real-Time Operating Systems", IEEE Transactions on Software Engineering, vol. 30, no. , pp. 613-629, September 2004, doi:10.1109/TSE.2004.45