Advertisement

A provably correct embedded verifier for the certification of safety critical software

  • Alessandro Cimatti
  • Fausto Giunchiglia
  • Paolo Pecchiari
  • Bruno Pietra
  • Joe Profeta
  • Dario Romano
  • Paolo Traverso
  • Bing Yu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

Vframe is one of Ansaldo's software driven vital architectures for safety critical products. This paper describes a project whose result is the development of an “embedded verifier”, i.e. a system integrated within Vframe and able to certify the correctness of one of Vframe components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end users.

Keywords

Virtual Machine Integer Variable Formal Verification Source Program Check Condition 
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

  1. 1.
    B. Boyer and Yu Y. Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor. In Proc. of the 11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, pages 416–430. Springer-Verlag, 1992.Google Scholar
  2. 2.
    R.S. Boyer and J.S. Moore. A Theorem Prover for a Computational Logic. In M. E. Stickel, editor, Proc. of the 10th Conference on Automated Deduction, pages 1–15, Kaiserlautern, Germany, July 1990. Published as Springer LNAI, number 449.Google Scholar
  3. 3.
    F. Giunchiglia, P. Pecchiari, and C. Talcott. Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report 9409-15, IRST, Trento, Italy, 1994.Google Scholar
  4. 4.
    D. Guaspari, C. Barbash, and D. Hoover. Checking critical code. Technical Report ORA TM-95-0081, Odyssey Research Associates, Ithaca, NY 14850 USA, September 1995.Google Scholar
  5. 5.
    M. Kaufmann and J. S. Moore. Design Goals for ACL2. Technical Report 101, Computational Logic Inc., Austin, Texas, 1994.Google Scholar
  6. 6.
    S. Kromodimoeljo, B. Pase, M. Saaltink, D. Craigen, and I. Meisels. The EVES system. In Proceedings of the International Lecture Series on “Functional Programming, Concurrency, Simulation and Automated Reasoning” (FPCSAR). McMaster University, August 1992.Google Scholar
  7. 7.
    J.S. Moore, editor. Special Issue on Systems Verification, Journal of Automated Reasoning. Vol. 5, n. 4, 1989.Google Scholar
  8. 8.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 20(2):107–125, February 1995.Google Scholar
  9. 9.
    J. Profeta, N. Andrianos, B. Yu, B. Jonson, T. DeLong, D. Guaspari, and D. Jamsek. Safety Critical Systems Built with COTS. Computer, 29(11):54–60, November 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Alessandro Cimatti
    • 1
  • Fausto Giunchiglia
    • 1
  • Paolo Pecchiari
    • 1
  • Bruno Pietra
    • 2
  • Joe Profeta
    • 3
  • Dario Romano
    • 2
  • Paolo Traverso
    • 1
  • Bing Yu
    • 3
  1. 1.Institute for Scientific and Technological ResearchIRSTPovoItaly
  2. 2.Ansaldo Trasporti SpaGenovaItaly
  3. 3.Ansaldo SignalPittsburgh

Personalised recommendations