Advertisement

Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information

  • Nurlida Basir
  • Ewen Denney
  • Bernd Fischer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5219)

Abstract

Formal methods can in principle provide the highest levels of assurance of code safety by providing formal proofs as explicit evidence for the assurance claims. However, the proofs are often complex and difficult to relate to the code, in particular if it has been generated automatically. They may also be based on assumptions and reasoning principles that are not justified. This causes concerns about the trustworthiness of the proofs and thus the assurance claims. Here we present an approach to systematically construct safety cases from information collected during a formal verification of the code, in particular from the construction of the logical annotations necessary for a formal, Hoare-style safety certification. Our approach combines a generic argument that is instantiated with respect to the certified safety property (i.e., safety claims) with a detailed, program-specific argument that can be derived systematically because its structure directly follows the course the annotation construction takes through the code. The resulting safety cases make explicit the formal and informal reasoning principles, and reveal the top-level assumptions and external dependencies that must be taken into account. However, the evidence still comes from the formal safety proofs. Our approach is independent of the given safety property and program, and consequently also independent of the underlying code generator. Here, we illustrate it for the AutoFilter system developed at NASA Ames.

Keywords

Automated code generation formal program verification Hoare logic fault tree analysis safety case Goal Structuring Notation 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    ASCE home page (2007), http://www.adelard.com/web/hnav/ASCE
  2. 2.
    Audsley, N.C., Bate, I.J., Crook-Dawkins, S.K.: Automatic Code Generation for Airborne Systems. In: Proc. of the IEEE Aerospace Conference, p. 11. IEEE, Los Alamitos (2003)Google Scholar
  3. 3.
    Basir, N., Denney, E., Fischer, B.: Deriving Safety Cases for the Formal Safety Certification of Automatically Generated Code. In: Huhn, M., Hungar, H. (eds.) SafeCert 2008 Intl. Workshop on the Certification of Safety-Critical Software Controlled Systems, ENTCS. Elsevier, Amsterdam (2008)Google Scholar
  4. 4.
    Bishop, P., Bloomfield, R.: A methodology for safety case development. In: Redmill, F., Anderson, T. (eds.) Industrial Perspectives of Safety-critical Systems: Proc. 6th Safety-critical Systems Symposium, pp. 194–203. Springer, Heidelberg (1998)Google Scholar
  5. 5.
    Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley, Reading (2000)Google Scholar
  6. 6.
    Denney, E., Fischer, B.: Correctness of source-level safety policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) Proc. FM 2003: Formal Methods. LNCS, vol. 2805, pp. 894–913. Springer, Heidelberg (2003)Google Scholar
  7. 7.
    Denney, E., Fischer, B.: Software certification and software certificate management systems (Position paper). In: Proc. ASE Workshop on Software Certificate Management Systems, pp. 1–5. ACM, New York (2005)Google Scholar
  8. 8.
    Denney, E., Fischer, B.: A generic annotation inference algorithm for the safety certification of automatically generated code. In: Jarzabek, S., Schmidt, D.C., Veldhuizen, T.L. (eds.) Proc. Conf. Generative Programming and Component Engineering, pp. 121–130. ACM, New York (2006)CrossRefGoogle Scholar
  9. 9.
    Denney, E., Fischer, B.: Annotation inference for safety certification of automatically generated code (extended abstract). In: Uchitel, S., Easterbrook, S. (eds.) Proc. 21st ASE, pp. 265–268. IEEE, Los Alamitos (2006)Google Scholar
  10. 10.
    Denney, E., Trac, S.: A Software Safety Certification Tool for Automatically Generated Guidance, Navigation and Control Code. In: Electronic Proc. IEEE Aerospace Conference. IEEE, Los Alamitos (2008)Google Scholar
  11. 11.
    Denney, E., Fischer, B.: Certifiable program generation. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 17–28. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Galloway, A., Paige, R.F., Tudor, N.J., Weaver, R.A., Toyn, I., McDermid, J.: Proof vs testing in the context of safety standards. In: The 24th Digital Avionics Systems Conference, vol. 2, p. 14. IEEE Press, Los Alamitos (2005)CrossRefGoogle Scholar
  13. 13.
    Hughes, W.: Critical Thinking. Broadview Press (1992)Google Scholar
  14. 14.
    Kelly, T.P.: Arguing safety a systematic approach to managing safety cases. PhD Thesis, University of York (1998)Google Scholar
  15. 15.
    Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)Google Scholar
  16. 16.
    Necula, G.C.: Proof-carrying code. In: Proc. 24th Conf. Principles of Programming Languages, pp. 106–119. ACM, New York (1997)Google Scholar
  17. 17.
    O’Halloran, C.: Issues for the automatic generation of safety critical software. In: Proc.15th Conf. Automated Software Engineering, pp. 277–280. IEEE, Los Alamitos (2000)Google Scholar
  18. 18.
    PolySpace Technologies, http://www.polyspace.com
  19. 19.
    Reif, W.: The KIV Approach to Software Verification. In: KORSO: Methods, Languages and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 339–370. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  20. 20.
    Reinhardt, D.W.: Use of the C++ Programming Language in Safety Critical Systems. Master Thesis, University of York (2004)Google Scholar
  21. 21.
    RTCA, Software Considerations in Airborne Systems and Equipment Certification. RTCA (1992)Google Scholar
  22. 22.
    Smith, D.R.: KIDS: A semi-automatic program development system. IEEE Trans. on Software Engineering 16(9), 286–290 (1990)CrossRefGoogle Scholar
  23. 23.
    Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libraries. In: Proc. 12th Conf. Automated Deduction. LNCS (LNAI), vol. 814, pp. 341–355. Springer, Heidelberg (1994)Google Scholar
  24. 24.
    Stürmer, I., Conrad, M.: Test suite design for code generation tools. In: Proc. 18th Conf. Automated Software Engineering, pp. 286–290. IEEE, Los Alamitos (2003)CrossRefGoogle Scholar
  25. 25.
    Stürmer, I., Weinberg, D., Conrad, M.: Overview of Existing Safeguarding Techniques for Automatically Generated Code. In: Proc. of 2nd Intl. ICSE Workshop on Software Engineering for Automotive Systems, pp. 1–6. ACM, New York (2006)Google Scholar
  26. 26.
    Weaver, R.A.: The Safety of Software–Constructing and Assuring Arguments. PhD Thesis, University of York (2003)Google Scholar
  27. 27.
    Whalen, M.W., Heimdahl, M.P.E.: On the requirements of High-Integrity Code Generation. In: Proc. 4th High Assurance in Systems Engineering Workshop, pp. 217–224. IEEE, Los Alamitos (1999)CrossRefGoogle Scholar
  28. 28.
    Whittle, J., Schumann, J.: Automating the implementation of Kalman filter algorithms. ACM Transactions on Mathematical Software 30(4), 434–453 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Wong, W.: Validation of HOL proofs by proof checking. Formal Methods in System Design: An International Journal 14, 193–212 (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Nurlida Basir
    • 1
  • Ewen Denney
    • 2
  • Bernd Fischer
    • 1
  1. 1.ECSUniversity of SouthamptonSouthamptonUK
  2. 2.NASA Ames Research CenterUSRA/RIACSMountain ViewUSA

Personalised recommendations