Another formal proof for Deadline Driven 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/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Zhan Naijun

Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00)

Cheju Island, South Korea

December 12-December 14

ISBN: 0-7695-0930-4

	ASCII Text	x
	Zhan Naijun, "Another formal proof for Deadline Driven Scheduler," Real-Time Computing Systems and Applications, International Workshop on, pp. 481, Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00), 2000.

	BibTex	x
	@article{ 10.1109/RTCSA.2000.896430, author = {Zhan Naijun}, title = {Another formal proof for Deadline Driven Scheduler}, journal ={Real-Time Computing Systems and Applications, International Workshop on}, volume = {0}, year = {2000}, issn = {1533-2306}, pages = {481}, doi = {http://doi.ieeecomputersociety.org/10.1109/RTCSA.2000.896430}, 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 - Another formal proof for Deadline Driven Scheduler SN - 1533-2306 SP EP A1 - Zhan Naijun, PY - 2000 KW - theorem proving; scheduling; process algebra; real-time systems; formal proof; Deadline Driven Scheduler; DDS correctness; duration calculus; DC; random preemption; induction rules; induction propositions; intuitive facts VL - 0 JA - Real-Time Computing Systems and Applications, International Workshop on ER -

Zhan Naijun, Inst. of Software, Acad. Sinica, Beijing, China

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

The paper presents another formal proof for the correctness of the Deadline Driven Scheduler (DDS). This proof is different from Zheng Yuhua and Zhou Chaochen's, although both are given in terms of duration calculus (DC) which provides abstraction for random preemption of processor. In the proof of Zheng and Zhou, the induction rules of the duration calculus are heavily applied, but the intuition of the induction propositions is not obvious. However, this proof is to follow and to formalise the original one developed by C.L. Liu and J.W. Layland (1973) which relies on many intuitive facts. Therefore, this proof is more intuitive, while it is still formal.

Index Terms:

theorem proving; scheduling; process algebra; real-time systems; formal proof; Deadline Driven Scheduler; DDS correctness; duration calculus; DC; random preemption; induction rules; induction propositions; intuitive facts

Citation:

Zhan Naijun, "Another formal proof for Deadline Driven Scheduler," rtcsa, pp.481, Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00), 2000

Peer Review Notice | Give Us Feedback

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