Abstract
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.
This research is supported by DeTfoRS Project funded by the National Hi-Tech Programme of China and UNU/IIST.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
B.Moszkowski: A Temporal Logic for Multi-level Reasoning about Hardware. In IEEE Computer, Vol.18(2),pp10–19, 1985.
J.U. SkakkebÆk, Natarajan Shankar: Towards a Duration Calculus Proof Assistant in PVS, ProCoS II Report ID/DTH JUS 5/1, March 1994
Zhou Chaochen, C.A.R. Hoare and A.P. Ravn, A Calculus of Durations, Information Processing Letters, 40(5):269–276, 1991.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yuhua, Z., Chaochen, Z. (1994). A formal proof of the Deadline Driven scheduler. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_194
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_194
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive