Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Architecting Critical Systems

ISARCS 2010: Architecting Critical Systems pp 72–88Cite as

A Road to a Formally Verified General-Purpose Operating System

  • Conference paper

  • 665 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 6150))

Abstract

Methods of formal description and verification represent a viable way for achieving fundamentally bug-free software. However, in reality only a small subset of the existing operating systems were ever formally verified, despite the fact that an operating system is a critical part of almost any other software system. This paper points out several key design choices which should make the formal verification of an operating system easier and presents a work-in-progress and initial experiences with formal verification of HelenOS, a state-of-the-art microkernel-based operating system, which, however, was not designed specifically with formal verification in mind, as this is mostly prohibitive due to time and budget constrains.

The contribution of this paper is the shift of focus from attempts to use a single “silver-bullet” formal verification method which would be able to verify everything to a combination of multiple formalisms and techniques to successfully cover various aspects of the operating system. A reliable and dependable operating system is the emerging property of the combination, thanks to the suitable architecture of the operating system.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World. Communications of the ACM 53(2), 66–75 (2010)

    Article  Google Scholar 

  2. Kofron, J.: Checking Software Component Behavior Using Behavior Protocols and Spin. In: Proceedings of Applied Computing 2007, Seoul, Korea, pp. 1513–1517 (2007)

    Google Scholar 

  3. GCC, the GNU Compiler Collection, http://gcc.gnu.org/

  4. Clang: a C language family frontend for LLVM, http://clang.llvm.org/

  5. Clang Static Analyzer, http://clang-analyzer.llvm.org/

  6. Bulej, L., Bures, T., Coupaye, T., Decky, M., Jezek, P., Parizek, P., Plasil, F., Poch, T., Rivierre, N., Sery, O., Tuma, P.: CoCoME in Fractal. In: Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.) The Common Component Modeling Example. LNCS, vol. 5153, pp. 357–387. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Coverity, http://scan.coverity.com/

  8. Mencl, V.: Deriving Behavior Specifications from Textual Use Cases. In: Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE 2004), Linz, Austria, September 21, part of ASE 2004, pp. 331–341. Oesterreichische Computer Gesellschaft (2004)

    Google Scholar 

  9. Frama-C, http://frama-c.cea.fr/

  10. Lawlis, P.K.: Guidelines for Choosing a Computer Language: Support for the Visionary Organization. Ada Information Clearinghouse (1998), http://archive.adaic.com/docs/reports/lawlis/k.htm

  11. HelenOS Project, http://www.helenos.org/

  12. Oplustil, T.: Inheritance in Architecture Description Languages. In: Reviewed section of Proceedings of the Week of Doctoral Students 2003 conference (WDS 2003), Charles University, Prague, Czech Republic, vol. 2003, pp. 124–131 (2003)

    Google Scholar 

  13. Operating System Market Share, http://marketshare.hitslink.com/report.aspx?qprid=8&qptimeframe=M&qpsp=132 (retrieved on 2010-02-28)

  14. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA (2009)

    Google Scholar 

  15. Spin, http://spinroot.com/

  16. Stanse: Static Analysis Framework for C code, http://stanse.fi.muni.cz/

  17. Valgrind, http://valgrind.org/

  18. VCC, http://vcc.codeplex.com/

Download references

Author information

Authors and Affiliations

  1. Department of Distributed and Dependable Systems, Faculty of Mathematics and Physics, Charles University, Malostranské náměstí 25, Prague 1, 118 00, Czech Republic

    Martin Děcký

Authors
  1. Martin Děcký
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Hasso Plattner Institute for Software Systems Engineering, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany

    Holger Giese

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Děcký, M. (2010). A Road to a Formally Verified General-Purpose Operating System. In: Giese, H. (eds) Architecting Critical Systems. ISARCS 2010. Lecture Notes in Computer Science, vol 6150. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13556-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13556-9_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13555-2

  • Online ISBN: 978-3-642-13556-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation