A formally verified application-level framework for real-time scheduling on POSIX real-time operating systems

Abstract

We present 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.