This paper presents an approach to formalizing and proving real-time properties of schedulers. The formal logic that we propose to use is the Duration Calculus [1], and the scheduler that we select here to serve as an example is the Deadline Driven Scheduling Algorithm [2]. The specification and proof of the algorithm are formulated abstractly by using the Duration Calculus. The result may encourage others to formally treat more real-time aspects of operating systems which are conventionally a piece of ad hoc territory in computer science.


scheduler real-time systems deadline driven algorithm duration calculus specification and verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M.R. Hansen and Zhou Chaochen, Semantics and Completeness of Duration Calculus, Proc. of Real-Time: Theory in Practice, REX Workshop, Mook, the Netherlands, LNCS 600, pp.209–225, 1992.Google Scholar
  2. 2.
    C.L.Liu and J.W.Layland. Scheduling Algorithms for Multiprogramming in a Hard Real-Time Environment. J. of ACM.20(1),pp. 46–61. 1973.Google Scholar
  3. 3.
    Liu Zhiming, Mathai Joseph and Tomasz Janowski, Verification of Schedulability for Real-Time Programs, Technical Report RR245, Department of Computer Science, University of Warwick,1993.Google Scholar
  4. 4.
    B.Moszkowski: A Temporal Logic for Multi-level Reasoning about Hardware. In IEEE Computer, Vol.18(2),pp10–19, 1985.Google Scholar
  5. 5.
    J.U. SkakkebÆk, Natarajan Shankar: Towards a Duration Calculus Proof Assistant in PVS, ProCoS II Report ID/DTH JUS 5/1, March 1994Google Scholar
  6. 6.
    Zhou Chaochen, C.A.R. Hoare and A.P. Ravn, A Calculus of Durations, Information Processing Letters, 40(5):269–276, 1991.Google Scholar
  7. 7.
    Zhou Chaochen, M.R.Hansen, A.P.Ravn, H.Rischel: Duration Specifications for Shared Processors, Proc.of the Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Nijmegen, January 1992. LNCS 571,pp 21–32, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Zheng Yuhua
    • 1
  • Zhou Chaochen
    • 1
  1. 1.International Institute for Software TechnologyThe United Nations UniversityMacau

Personalised recommendations