Abstract
This paper reports the experience of the Software Engineering Laboratory of the National Research Council of Canada with the modelling and verification of the kernel of Harmony, a portable real-time multitasking multiprocessor operating system. In this paper we explain the aim of this study and give the first results. We use a modelling approach and formalize the models of the system, the scenarios and the properties that are to be checked in PROMELA using the SPIN tool. Several models of the systems were produced with various degrees of abstraction and completeness. The most recent is a tractable one that enables the expression, simulation and verification of any scenario that consists of a bounded number of tasks that may use all the services of the kernel. An exhaustive verification of the intertask communication features of Harmony was carried out by model-checking. It revealed a bug that has been in the system for more than ten years. The first verifications of the dynamic task management primitives lead to the discovery of other bugs and serious critical races. This paper shows that it is possible to detect more than deadlocks when using formal methods for the study of a real medium-sized operating system that encompasses complex internal management.
This research was done at the Software Engineering Laboratory, National Research Council of Canada, Ottawa, Ontario, Canada K1A OR6, and is registered as technical report NRC 38309.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andrews D. & Ince D., Practical Formal Methods with VDM, McDrawhill Int., 1991.
Audureau-Enjalbert-Fariñas, Logique temporelle, semantique et validation des programmes paralleles, Masson, 1990.
Badel M, Duong D., Eyraud S., The New Simulation Facilities in QNAP2, Proc of ESS91, Het Pand, Belgium, November 1991.
Birrell A.D., Guttag J.V., Horning J.J. & Levin R., Synchronization Primitives for a Multiprocessor, A Formal Specification, Operating Systems Review, 21 (5), 1987.
Doeppner T.W. & Giacalone A., A Formal Description of the UNIX Operating System, Proc. of 2nd ACM Symp. on Principles of Distrib. Syst., Montreal, Canada, August 1983.
Gauthier C., Design and Implementation of Realtime Operating System on Thinwire Multiprocessor, PhD candidacy paper, Ottawa University, June 1993.
Gentleman W.M., MacKay S.A., Stewart D.A. & Wein M., Using the Harmony Operating System, Release 3.0, NRC/ERA-377, National Research Council of Canada, Ottawa, February 1989.
Gerhart S., Craigen D. & Ralston T., Experience with Formal Methods in Critical Systems, IEEE Software, January 1994, pp. 21–39.
Glade B.B., A temporal logic to Promela “never” clause converter, EE594 Final Project, Cornell University, Electrical Engin. Department, 3 May 1991.
Gotzhein R., Temporal Logic and applications — a tutorial, Computer Networks and ISDN Systems 24(1992) 203–218.
Gouda M.G., Protocol verification made simple: a tutorial Computer Networks, 25(9), April 93, pp. 969–980.
Holzmann G J, Algorithms for automated protocol verification, AT&T Technical Journal Jan/Feb, 1990
Holzmann G.J., Basic Spin Manual, AT&T Bell Laboratories, March 1994.
Holzmann G J, Design and Validation of Computer Protocols, 512 pgs, ISBN 0–13–539925–4, Publ. Prentice Hall, (c ) 1991 AT&T Bell Laboratories.
Holzmann G.J., Design and validation of protocols: a tutorial Computer Networks, 25(9), April 93, pp. 981–1017.
Jones C.B., Systematic Software Development Using VDM, Prentice Hall Inter., 1990
Lai R. & Jirachiefpattana A., Verification of ISO ACSE protocol specified in Estelle, Computer Communication 17(3), March 1994.
Li Y., The Harmony operating system described by Petri nets, Master thesis, Carleton University, 1987.
NRC, Harmony Operating System, Release 4.0, Application Note 18, National Research Council of Canada, Ottawa, Ont., March 1993.
Ousterhout J., Tcl and the Tk toolkit, Addison-Wesley, 1994.
Pêcheur C., Using Lotos for specifying the CHORUS distributed operating system kernel, Computer Communication 15(2), Mars 1992.
Pike R., Presotto D., Thompson K. & Holzmann G., Process Sleep and Wakeup on Shared-memory Multiprocessor, EurOpen’91 — Tromso
Ramsey N., Correctness of Trap-Based Breakpoint Implementations, Bell Communications Research, November 1993.
Spivey J.M., Specifying a Real-Time Kernel, IEEE Software, 7(5), 1990.
West C.H., Protocol Validation — principles and applications, Computer Networks and ISDN Systems 24, 1992, pp. 219–242.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Cattel, T. (1995). Modelling and Verification of a Multiprocessor Realtime OS Kernel. In: Hogrefe, D., Leue, S. (eds) Formal Description Techniques VII. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34878-0_4
Download citation
DOI: https://doi.org/10.1007/978-0-387-34878-0_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2881-0
Online ISBN: 978-0-387-34878-0
eBook Packages: Springer Book Archive