Skip to main content
SpringerLink
Log in

On the Architecture of System Verification Environments

  • Conference paper
Hardware and Software: Verification and Testing (HVC 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4899))

Included in the following conference series:

Abstract

Implementations of computer systems comprise many layers and employ a variety of programming languages. Building such systems requires support of an often complex, accompanying tool chain.

The Verisoft project deals with the formal pervasive verification of computer systems. Making use of appropriate formal specification and proof tools, this task requires (i) specifying the layers and languages used in the implementation, (ii) specifying and verifying the algorithms employed by the tool chain (or, alternatively, validating their actual output), and (iii) proving simulation statements between layers, arguing about the programs residing at the different layers. Combining the simulation statements for all layers should allow to transfer correctness results for top-layer programs to their bottom-layer representation; in this manner, a verified stack can be built.

Maintaining all formal artifacts, the actual system implementation, and the (verification) tool chain is a challenging task. We call sets of tools that help addressing this task system verification environments. In this paper, we describe the structure, contents, and architecture of the system verification environment used in the Verisoft project.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Winskel, G.: The formal semantics of programming languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  2. Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction. John Wiley & Sons, Chichester (1992)

    MATH  Google Scholar 

  3. Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580 (1969)

    Article  MATH  Google Scholar 

  4. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, 453–457 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  5. Gries, D.: The Science of Programming. Springer, Heidelberg (1987)

    MATH  Google Scholar 

  6. The Verisoft Project. http://www.verisoft.de/

  7. Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5, 411–428 (1989)

    Google Scholar 

  8. Moore, J S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 161–172. Springer, Heidelberg (2003)

    Google Scholar 

  9. de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Univ. Press, Cambridge, UK (2001)

    MATH  Google Scholar 

  10. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  11. Mueller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)

    MATH  Google Scholar 

  12. Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, Springer, Heidelberg (2003)

    Google Scholar 

  13. Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Francisco (1996)

    MATH  Google Scholar 

  14. Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: Aichernig, B., Beckert, B. (eds.) SEFM 2005, pp. 2–11 (2005)

    Google Scholar 

  15. Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 1–16. Springer, Heidelberg (2005)

    Google Scholar 

  16. Dörrenbächer, J.: (VAMOS microkernel, formal models and verification) Talk given at the International Workshop on System Verification, SV 2006, Sydney, Australia (August 7–8, 2006), http://www.cse.unsw.edu.au/~formalmethods/events/svws-06/VAMOS_Microkernel.pdf

  17. Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309–316. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  18. Knapp, S., Paul, W.: Realistic Worst Case Execution Time Analysis in the Context of Pervasive System Verification. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 53–81. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Knapp, S., Paul, W.: Pervasive verification of distributed real-time systems. In: Broy, M., Grünbauer, J., Hoare, T. (eds.) Software System Reliability and Security, Trento, Italy. NATO Security Through Science Series. Sub-Series D: Information and Communication Security, vol. 9, pp. 239–297. IOS Press, Amsterdam, Trento, Italy (2007)

    Google Scholar 

  20. Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Beckert, B. (ed.) Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, pp. 4–20 (2007)

    Google Scholar 

  21. Schmaltz, J.: A formal model of lower system layer. In: Gupta, A., Manolios, P. (eds.) FMCAD 2006, pp. 191–192. IEEE Computer Society, Los Alamitos (2006)

    Google Scholar 

  22. Knapp, S.: Towards the verification of functional and timely behavior of an eCall implementation. Master’s thesis, Saarland Univ. (2005), http://www-wjp.cs.uni-sb.de/publikationen/Knapp05.pdf

    Google Scholar 

  23. Botaschanjan, J., Gruler, A., Harhurin, A., Kof, L., Spichkova, M., Trachtenherz, D.: Towards modularized verification of distributed time-triggered systems. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 163–178. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  24. Dalinger, I., Hillebrand, M., Paul, W.: On the verification of memory management mechanisms. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 301–316. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Starostin, A.: Formal verification of a C-library for strings. Master’s thesis, Saarland Univ. (2006), http://www-wjp.cs.uni-sb.de/publikationen/St06.pdf

  26. Fischer, S.: Formal verification of a big integer library including division. Master’s thesis, Saarland University (2007)

    Google Scholar 

  27. Appel, A.W., Ginsburg, M.: Modern Compiler Implementation in C. Cambridge Univ. Press, New York (1998)

    Google Scholar 

  28. Liedtke, J.: On micro-kernel construction. In: SOSP 1995. Proceedings of the 15th ACM Symposium on Operating systems principles, pp. 237–250. ACM Press, New York (1995)

    Chapter  Google Scholar 

  29. Shadrin, A.: Design and implementation of the portmapper and RPC primitives in the context of the SOS. Master’s thesis, Saarland Univ. (2006), http://www-wjp.cs.uni-sb.de/publikationen/Sh06.pdf

    Google Scholar 

  30. Langenstein, B., Nonnengart, A., Rock, G., Stephan, W.: A history-based verification of distributed applications. In: Beckert, B. (ed.) Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, pp. 70–84 (2007)

    Google Scholar 

  31. Beuster, G., Henrich, N., Wagner, M.: Real world verification – Experiences from the Verisoft email client. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR Workshop Proceedings. CEUR-WS.org, vol. 192, pp. 112–125 (2006)

    Google Scholar 

  32. Lindenberg, C., Wirt, K., Buchmann, J.: (Formal proof for the correctness of RSA-PSS) Cryptology ePrint Archive, Report 2006/011, http://eprint.iacr.org/2006/011

  33. Cheikhrouhou, L., Rock, G., Stephan, W., Schwan, M., Lassmann, G.: Verifying a chipcard-based biometric identification protocol in VSE. In: Górski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 42–56. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A.: Verification Support Environment. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 476–493. Springer, Heidelberg (2005)

    Google Scholar 

  35. Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technical University of Munich (2006)

    Google Scholar 

  36. Tverdyshev, S.: Combination of Isabelle/HOL with automatic tools. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 302–309. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  37. ACSAR: Automatic Checker of Safety properties based on Abstraction Refinement. http://www.mpi-inf.mpg.de/~seghir/ACSAR/ACSAR-web-page.html

  38. ARMC: Abstraction refinement-based model checker for safety and liveness properties. http://www.mpi-inf.mpg.de/~rybal/armc/

  39. Jahob and Bohne: Verifying data structure consistency. http://www.mit.edu/~vkuncak/projects/jahob/

  40. Daum, M., Maus, S., Schirmer, N., Seghir, M.N.: Integration of a software model checker into Isabelle. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 381–395. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  41. Emeliyanenko, P.: Automatic verification of conditions for absence of interrupts. Bachelor’s thesis, Saarland Univ. (2006) http://react.cs.uni-sb.de/fileadmin/user_upload/react/theses/PEmeliyanenko.pdf .

  42. SPASS: An Automated Theorem Prover for First-Order Logic with Equality. http://spass.mpi-sb.mpg.de/

  43. e-SETHEO prover system. http://www4.in.tum.de/~stenzg/

  44. Ferdinand, C., Heckmann, R.: Verifying timing behavior by abstract interpretation of executable code. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 336–339. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  45. Subversion: An open-source revision control system. http://subversion.tigris.org/

  46. Petrova, E.: Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Computer Science Department (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. German Research Center for Artificial Intelligence (DFKI), P.O. Box 15 11 50, 66041, Saarbrücken, Germany

    Mark A. Hillebrand

  2. Saarland University, P.O. Box 15 11 50, 66041, Saarbrücken, Germany

    Wolfgang J. Paul

Authors
  1. Mark A. Hillebrand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wolfgang J. Paul
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Karen Yorav

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hillebrand, M.A., Paul, W.J. (2008). On the Architecture of System Verification Environments. In: Yorav, K. (eds) Hardware and Software: Verification and Testing. HVC 2007. Lecture Notes in Computer Science, vol 4899. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77966-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-77966-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-77966-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation