|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA'99)
A Formal Proof of the Rate Monotonic Scheduler
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," 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 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 ={2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications}, 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 - 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications 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 - 2012 IEEE International Conference on Embedded and Real-Time Computing Systems and Applications ER - | |||
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
Usage of this product signifies your acceptance of the Terms of Use.