Abstract
Though program verification is known and has been used for decades, the verification of a complete computer system still remains a grand challenge. Part of this challenge is the interaction of application programs with the operating system, which is usually entrusted with retrieving input data from and transferring output data to peripheral devices. In this scenario, the correct operation of the applications inherently relies on operating-system correctness. Based on the formal correctness of our real-time operating system Olos, this paper describes an approach to pervasively verify applications running on top of the operating system.
Work partially funded by the German Federal Ministry of Education and Research (BMBF) in the framework of the Verisoft project under grant 01 IS C38.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Vartabedian, R., Bensinger, K.: Doubt cast on Toyota’s decision to blame sudden acceleration on gas pedal defect, Los Angeles Times (January 30, 2010)
Guynn, J.: Apple co-founder Steve Wozniak says his Toyota Prius accelerates on its own, Los Angeles Times (February 3, 2010)
Moore, J.S.: A grand challenge proposal for formal methods: A verified stack. In: 10th Anniversary Colloquium of UNU/IIST, pp. 161–172. Springer, Heidelberg (2002)
Klein, G.: Operating system verification — an overview. Sādhanā 34(1), 27–69 (2009)
Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.J.: Putting it all together: Formal verification of the VAMP. STTT 8(4-5), 411–430 (2006)
In der Rieden, T., Tsyban, A.: CVM – a verified framework for microkernel programmers. In: Huuck, R., Klein, G., Schlich, B. (eds.) Systems Software Verification. ENTCS, vol. 217, pp. 151–168. Elsevier Science B.V., Amsterdam (2008)
Daum, M., Schirmer, N.W., Schmidt, M.: Implementation correctness of a real-time operating system. In: van Hung, D., Krishnan, P. (eds.) SEFM, pp. 23–32. IEEE Computer Society, Los Alamitos (2009)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Alkassar, E., Hillebrand, M.A., Leinenbach, D.C., Schirmer, N.W., Starostin, A., Tsyban, A.: Balancing the load – leveraging a semantics stack for systems verification. J. Autom. Reasoning 42(2-4), 389–454 (2009)
Leinenbach, D., Petrova, E.: Pervasive compiler verification: From verified programs to verified systems. In: Huuck, R., Klein, G., Schlich, B. (eds.) Systems Software Verification. ENTCS, vol. 217, pp. 23–40. Elsevier Science B.V., Amsterdam (2008)
Schirmer, N.W.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, TU Munich (2006)
Kopetz, H., Grünsteidl, G.: TTP – A protocol for fault-tolerant real-time systems. IEEE Computer 27(1), 14–23 (1994)
American National Standards Institute: ANSI ISO IEC 9899-1999: Programming Languages — C. American National Standards Institute, New York, USA (1999)
Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N., Starostin, A.: The Verisoft approach to systems verification. In: Verified Software: Theories, Tools, and Experiments. Volume 5295 of LNCS., Springer (2008) 209–224
Starostin, A., Tsyban, A.: Correct microkernel primitives. In: Huuck, R., Klein, G., Schlich, B. (eds.) Systems Software Verification. ENTCS, vol. 217, pp. 169–185. Elsevier Science B.V., Amsterdam (2008)
Heckmann, R., Ferdinand, C.: Worst-case execution time prediction by static program analysis. White paper, AbsInt Angewandte Informatik GmbH (2004)
Bevier, W.R.: Kit and the short stack. J. Autom. Reasoning 5(4), 519–530 (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Daum, M., Schirmer, N.W., Schmidt, M. (2010). From Operating-System Correctness to Pervasively Verified Applications. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-16265-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16264-0
Online ISBN: 978-3-642-16265-7
eBook Packages: Computer ScienceComputer Science (R0)