This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Formally Verified Application-Level Framework for Real-Time Scheduling on POSIX Real-Time Operating Systems
September 2004 (vol. 30 no. 9)
pp. 613-629
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.

[1] FSMLabs, RT-Linux,http:/www.fsmlabs.com, 1997.
[2] L.P. Barreto, R. Douence, G. Muller, and M. Sudholt, Programming OS Schedulers with Domain-Specific Languages and Aspects: New Approaches for OS Kernel Engineering Proc. AOSD Workshop Aspects, Components, and Patterns for Infrastructure Software, Apr. 2002.
[3] G. Bollella and J. Gosling, "The Real-Time Specification for Java," Computer, vol. 33, no. 6, June 2000, pp. 47-54.
[4] G. Buttazzo and J. Stankovic, Adding Robustness in Dynamic Preemptive Scheduling Responsive Computer Systems: Steps Toward Fault-Tolerant Real-Time Systems, D. Fussel and M. Malek, eds., pp. 67-88, Oct. 1995.
[5] G.C. Buttazzo, The S.Ha.R.K. Project http://shark.sssup.itindex.shtml, 2004.
[6] K. Chen and P. Muhlethaler, A Scheduling Algorithm for Tasks Described by Time Value Function J. Real-Time Systems, vol. 10, no. 3, pp. 293-312, 1996.
[7] H. Chua and K. Nahrstedt, CPU Service Classes for Multimedia Applications Proc. IEEE Int'l Conf. Multimedia Computing and Systems, June 1999.
[8] R. Clark, E.D. Jensen, A. Kanevsky, J. Maurer, P. Wallace, T. Wheeler, Y. Zhang, D. Wells, T. Lawrence, and P. Hurley, An Adaptive, Distributed Airborne Tracking System Proc. IEEE Int'l Workshop Parallel and Distributed Real-Time Systems, pp. 353-362, 1999.
[9] R.K. Clark, Scheduling Dependent Real-Time Activities PhD dissertation, Carnegie Mellon Univ., 1990.
[10] Z. Deng, J.W.-S. Liu, and J. Sun, “A Scheme for Scheduling Hard Real-Time Applications in Open System Environment,” Proc. Ninth Euromicro Workshop Real-Time Systems, pp. 191-199, June 1997.
[11] S. Feizabadi, W. Beebee Jr., B. Ravindran, P. Li, and M. Rinard, Utility Accrual Scheduling with Real-Time Java Proc. Workshop Java Technologies for Real-Time and Embedded Systems, 2003.
[12] C.D. Gill, D.L. Levine, and D.C. Schmidt, The Design and Performance of a Real-Time CORBA Scheduling Service Real-Time Systems, vol. 20, no. 2, pp. 3-40, Mar. 2001.
[13] P. Goyal, X. Guo, and H. Vin, A Hierarchical CPU Scheduler for Multimedia Operating Systems Proc. USENIX OSDI Symp., pp. 107-121, 1996.
[14] C.A.R. Hoare, Communicating Sequential Processes Comm. ACM, vol. 21, no. 8, pp. 666-677, 1978.
[15] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[16] W. Horn, Some Simple Scheduling Algorithms Naval Research Logistics Quaterly, vol. 21, pp. 177-185, 1974.
[17] IEEE and The Open Group, The Open Group Base Specifications Issue 6, 2001.
[18] E.D. Jensen, Distributed Real-Time Specification (jsr50) http://jcp.org/en/jsrdetail?id=050, 2000.
[19] E.D. Jensen, C.D. Locke, and H. Tokuda, A Time-Driven Scheduling Model for Real-Time Systems Proc. IEEE Real-Time Systems Symp., pp. 112-122, Dec. 1985.
[20] G. Koren and D. Shasha, “D-Over: An Optimal On-Line Scheduling Algorithm for Overloaded Real-Time Systems,” Proc. IEEE Real-Time Systems Symp., pp. 290-299, Dec. 1992.
[21] T.W. Kuo and C.H. Li, A Fixed-Priority-Driven Open Environment for Real-Time Applications Proc. IEEE 20th Real-Time Systems Symp., 1999.
[22] K.G. Larsen, P. Pettersson, and W. Yi, UPPAAL in a Nutshell Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1/2, pp. 134-152, 1997.
[23] I. Leslie, D. McAuley, R. Black, T. Roscoe, P. Barham, D. Evers, R. Fairbairns, and E. Hyden, “The Design and Implementation of an Operating System to Support Distributed Multimedia Applications,” IEEE J. Selected Areas in Comm., June 1997.
[24] P. Li, H. Cho, B. Ravindran, and E.D. Jensen, Scheduling Distributable Real-Time Threads in Tempus Middleware Proc. IEEE Int'l Conf. Parallel and Distributed Systems, pp. 187-194, 2004.
[25] P. Li, B. Ravindran, and T. Hegazy, Implementation and Evaluation of a Best-Effort Scheduling Algorithm in an Embedded Real-Time System Proc. IEEE Int'l Symp. Performance Analysis of Systems and Software, pp. 22-29, 2001.
[26] C.L. Liu and J.W. Layland, Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environment J. ACM, vol. 20, no. 1, pp. 46-61, 1973.
[27] C.D. Locke, Best-Effort Decision Making for Real-Time Scheduling PhD dissertation, Carnegie Mellon Univ., 1986.
[28] D.P. Maynard, S.E. Shipman, R.K. Clark, J.D. Northcutt, R.B. Kegley, B.A. Zimmerman, and P.J. Keleher, An Example Real-Time Command, Control, and Battle Management Application for Alpha Archons Project Technical Report 88121, CMU Computer Science Dept., Dec. 1988.
[29] C. Mercer and R. Rajkumar, An Interactive Interface and RT-Mach Support for Monitoring and Controlling Resource Management Proc. IEEE Real-Time and Embedded Technology and Applications Symp., 1995.
[30] Object Management Group, Real-Time CORBA 1.0 (joint submission) 1998.
[31] Dynamic Scheduling Real-Time CORBA 2.0 (joint revised submission) 2001.
[32] S. Oikawa and R. Rajkumar, Linux/RK: A Portable Resource Kernel in Linux Proc. IEEE Real-Time and Embedded Technology and Applications Symp., 1999.
[33] QNX Software Systems Ltd., QNX Neutrino OS version 6.2.0 http:/www.qnx.com/, 2002.
[34] R. Rajkumar, K. Juvva, A. Molano, and S. Oikawa, Resource Kernels: A Resource-Centric Approach to Real-Time Systems Proc. SPIE/ACM Conf. Multimedia Computing and Networking, 1998.
[35] J. Regehr and J.A. Stankovic, HLS: A Framework for Composing Soft Real-Time Schedulers Proc. IEEE Real-Time Systems Symp., pp. 3-14, 2001.
[36] M.A. Rivas and M.G. Harbour, POSIX-Compatible Application-Defined Scheduling in MaRTE OS Proc. Euromicro Conf. Real-Time Systems, pp. 67-75, June 2000.
[37] M. Singhal and N.G. Shivaratri, Advanced Concepts in Operating Systems. McGraw-Hill, 1994.
[38] D. Stewart and P. Khosla, Real-Time Scheduling of Sensor Based Control Systems Proc. IFAC/IFIP Workshop, pp. 139-144, May 1991.
[39] The Open Group Research Institute's Real-Time Group, MK7.3a Release Notes Cambridge, Mass.: The Open Group Research Inst., Oct. 1998.
[40] J. Wang and B. Ravindran, Time-Utility Function-Driven Switched Ethernet: Packet Scheduling Algorithm, Implementation, and Feasibility Analysis IEEE Trans. Parallel and Distributed Systems, vol. 15, no. 1, pp. 1-15, Jan. 2004.
[41] Y.-C. Wang and K.-J. Lin, "Implementing a General Real-Time Scheduling Framework in the RED-Linux Real-Time Kernel," Proc. 20th IEEE Real-Time Systems Symp., IEEE CS Press, Los Alamitos, Calif., 1999, pp. 246-255.
[42] J.W. Wendorf, Implementation and Evaluation of a Time-Driven Scheduling Processor Proc. IEEE Real-Time Systems Symp., pp. 172-180, December 1988.
[43] Wind River Systems, VxWorks 5.x http:/www.windriver. com, 2003.
[44] S. Yovine, Kronos: A Verification Tool for Real-Time Systems Int'l J. Software Tools for Technology Transfer, vol. 1, no. 1/2, pp. 123-133, 1997.
[45] E.D. Jensen and J.D. Northcutt, Alpha: A Non-Proprietary Operating System for Large, Complex, Distributed Real-Time Systems Proc. IEEE Workshop Experimental Distributed Systems, pp. 35-41, 1990.

Index Terms:
Real-time scheduling, time/utility functions, utility accrual scheduling, Portable Operating System Interface (POSIX), model checking.
Citation:
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. 9, pp. 613-629, Sept. 2004, doi:10.1109/TSE.2004.45
Usage of this product signifies your acceptance of the Terms of Use.