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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
ASCE home page (2007), http://www.adelard.com/web/hnav/ASCE
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)
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)
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)
Czarnecki, K., Eisenecker, U.W.: Generative Programming: Methods, Tools, and Applications. Addison-Wesley, Reading (2000)
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)
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)
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)
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)
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)
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)
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)
Hughes, W.: Critical Thinking. Broadview Press (1992)
Kelly, T.P.: Arguing safety a systematic approach to managing safety cases. PhD Thesis, University of York (1998)
Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)
Necula, G.C.: Proof-carrying code. In: Proc. 24th Conf. Principles of Programming Languages, pp. 106–119. ACM, New York (1997)
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)
PolySpace Technologies, http://www.polyspace.com
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)
Reinhardt, D.W.: Use of the C++ Programming Language in Safety Critical Systems. Master Thesis, University of York (2004)
RTCA, Software Considerations in Airborne Systems and Equipment Certification. RTCA (1992)
Smith, D.R.: KIDS: A semi-automatic program development system. IEEE Trans. on Software Engineering 16(9), 286–290 (1990)
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)
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)
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)
Weaver, R.A.: The Safety of Software–Constructing and Assuring Arguments. PhD Thesis, University of York (2003)
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)
Whittle, J., Schumann, J.: Automating the implementation of Kalman filter algorithms. ACM Transactions on Mathematical Software 30(4), 434–453 (2004)
Wong, W.: Validation of HOL proofs by proof checking. Formal Methods in System Design: An International Journal 14, 193–212 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basir, N., Denney, E., Fischer, B. (2008). Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information. In: Harrison, M.D., Sujan, MA. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2008. Lecture Notes in Computer Science, vol 5219. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87698-4_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-87698-4_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87697-7
Online ISBN: 978-3-540-87698-4
eBook Packages: Computer ScienceComputer Science (R0)