A Formal Proof of the Rate Monotonic Scheduler

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Dong Shuzhen Articles by Xu Qiwen Articles by Zhan Naijun

Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99)

Hong Kong, China

December 13-December 15

ISBN: 0-7695-0306-3

	ASCII Text	x
	Dong Shuzhen, Xu Qiwen, Zhan Naijun, "A Formal Proof of the Rate Monotonic Scheduler," Real-Time Computing Systems and Applications, International Workshop on, pp. 500, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999.

	BibTex	x
	@article{ 10.1109/RTCSA.1999.811306, author = {Dong Shuzhen and Xu Qiwen and Zhan Naijun}, title = {A Formal Proof of the Rate Monotonic Scheduler}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {1999}, issn = {1530-1427}, pages = {500}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811306}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Real-Time Computing Systems and Applications, International Workshop on TI - A Formal Proof of the Rate Monotonic Scheduler SN - 1530-1427 SP EP A1 - Dong Shuzhen, A1 - Xu Qiwen, A1 - Zhan Naijun, PY - 1999 KW - Scheduling KW - Feasibility KW - Logic KW - Duration Calculus KW - Formal Proof VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

Dong Shuzhen, United Nations University

Xu Qiwen, United Nations University

Zhan Naijun, United Nations University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTCSA.1999.811306

We formally prove Liu and Layland's classic theorem on the Rate Monotonic Scheduler in Duration Calculus, a real time interval temporal logic. We describe the assumption of the system, the scheduling policy, the requirement, i.e., service is met for the processes before their deadlines, all by Duration Calculus formulae. That a feasibility condition is sufficient is formalized as logical implication. By using the proof system of Duration Calculus, we formally prove that the feasibility condition due to Liu and Layland is sufficient.

Index Terms:

Scheduling, Feasibility, Logic, Duration Calculus, Formal Proof

Citation:

Dong Shuzhen, Xu Qiwen, Zhan Naijun, "A Formal Proof of the Rate Monotonic Scheduler," rtcsa, pp.500, Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99), 1999

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.