Skip to main content
SpringerLink
Log in

Towards applying the composition principle to verify a microkernel operating system

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1125))

Included in the following conference series:

Abstract

A compositional proof method allows the components of a system to be specified and verified independently, instead of having to verify the entire system as a monolithic unit. This paper describes how the composition principle of Abadi and Lamport can be applied to specify and compose systems that consist of both safety and progress properties, using the HOL theorem proving system. We discuss the translation of the composition principle into HOL and the resulting proof obligations, and introduce an example system, modeled after a microkernel operating system, that we composed using the method.

This work was sponsored by DARPA under contract USN N00014-93-1-1322 with the Office of Naval Research and by the National Security Agency’s UR Program.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253–284, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  2. Martín Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(3):73–132, January 1993.

    Article  Google Scholar 

  3. Martín Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.

    Article  Google Scholar 

  4. Willam R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382–1396, November 1989.

    Article  Google Scholar 

  5. William R. Bevier, Warren A. Hunt, Jr., J. Strother Moore, and William D. Young. An approach to systems verification. Journal of Automated Reasoning, 5:411–428, 1989.

    Google Scholar 

  6. Pierre Collette. Application of the composition principle to unity-like specifications. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT’ 93: Theory and Practice of Software Development, number 668 in Lecture Notes in Computer Science, pages 230–242. Springer-Verlag, April 1993.

    Google Scholar 

  7. M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higer Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  8. Judith A. Hemenway and Dr. Jonathan Fellows. Applying the Abadi-Lamport composition theorem in real-world secure system integration environments. In Proceedings of the Tenth Annual Computer Security Applications Conference, pages 44–53, December 1994.

    Google Scholar 

  9. Leslie Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1):32–45, January 1989.

    Article  MathSciNet  Google Scholar 

  10. Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  11. C. Zhang, R. Shaw, M. R. Heckman, G. D. Benson, M. Archer, K. Levitt, and R. A. Olsson. Towards a formal verification of a secure distributed system and its applications. In Proceedings of the 17th National Computer Security Conference, Baltimore, October 1994.

    Google Scholar 

  12. C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson. Mechanizing a programming logic for the concurrent programming language microSR in HOL. In Proceedings of the International Higher-Order-Logic Theorem Proving Workshop, pages 31–44, Vancouver, B.C., August 1993.

    Google Scholar 

  13. Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl Levitt, and Ron A. Olsson. A hierarchical method for reasoning about distributed programming languages. In E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, editors, Higher-Order-Logic Theorem Proving and Its Applications: 8th International Workshop, number 668 in Lecture Notes in Computer Science, pages 385–400, Aspen Grove, Utah, September 1995. Springer-Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of California, 95616, Davis, CA, USA

    Mark R. Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt & Ron A. Olsson

Authors
  1. Mark R. Heckman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cui Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Brian R. Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Dave Peticolas
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Karl N. Levitt
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Ron A. Olsson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gerhard Goos Juris Hartmanis Jan van Leeuwen Joakim von Wright Jim Grundy John Harrison

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heckman, M.R., Zhang, C., Becker, B.R., Peticolas, D., Levitt, K.N., Olsson, R.A. (1996). Towards applying the composition principle to verify a microkernel operating system. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1996. Lecture Notes in Computer Science, vol 1125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105408

Download citation

  • DOI: https://doi.org/10.1007/BFb0105408

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61587-3

  • Online ISBN: 978-3-540-70641-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation