Abstract
We present an equational verification of Milner's scheduler, which we checked by computer. To our knowledge, this is the first time that the scheduler is proof-checked for a general number n of scheduled processes.
The work of the first author took place in the context of EC Basic Research Action 7166 concur 2. The work of the second author is supported by the Netherlands Computer Science Research Foundation (SION) with financial support of the Netherlands Organisation for Scientific Research (NWO).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.
M. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report Logic Group Preprint Series No. 88, Utrecht University, 1993.
T. Coquand and G. Huet. The calculus of constructions. Information and Control, 76:95–120, 1988.
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA — Rocquencourt, May 1993.
H. Ehrig and B. Mahr. Fundamentals of algebraic specifications I, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
J.-C. Fernandez, A. Kerbrat and L. Mounier. Symbolic Equivalence Checking. In C. Courcoubetis, editor, Proceedings of the 5th International Conference, CAV '93, Elounda, Greece, volume 697 of Lecture Notes in Computer Science, pages 85–97. Springer-Verlag, 1993.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1989.
R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89, pages 613–618. North-Holland, 1989.
J.F. Groote and H. Korver. A correctness proof of the bakery protocol in μCRL. Technical Report Logic Group Preprint Series No. 80, Utrecht University, 1992.
J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer checked verification. Technical Report 100, Logic Group Preprint Series, Utrecht University, October 1993.
J.F. Groote and A. Ponse. The syntax and semantics of μCRL. Technical Report CS-R9076, CWI, Amsterdam, 1990.
J.F. Groote and A. Ponse. Proof theory for μCRL. Technical Report CS-R9138, CWI, Amsterdam, 1991.
J.F. Groote and A. Ponse. μCRL: A base for analysing processes with data. In E. Best and G. Rozenberg, editors, Proceedings 3rd Workshop on Concurrency and Compositionality, Goslar, GMD-Studien Nr. 191, pages 125–130. Universität Hildesheim, 1991.
L. Helmink, M.P.A. Sellink, and F. Vaandrager. Proof-checking a data link protocol. 1993. To appear.
H. Korver and J. Springintveld. A Computer-Checked Verification of Milner's Scheduler. Technical Report Logic Group Preprint Series No. 101, Utrecht University, November, 1993. Full version.
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer-Verlag, 1993.
M.P.A. Sellink. Verifying process algebra proofs in type theory. Technical Report Logic Group Preprint Series No. 87, Utrecht University, 1993.
N.V. Stenning. A data transfer protocol. Computer Networks. 1:99–110, 1976.
A.S. Tanenbaum. Computer networks. Prentice-Hall International, Englewood Cliffs, 1989.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korver, H., Springintveld, J. (1994). A computer-checked verification of Milner's scheduler. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_95
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive