Abstract
Formal certification is based on the idea that a mathematical proof of some property of a piece of software can be regarded as a certificate of correctness which, in principle, can be subjected to external scrutiny. In practice, however, proofs themselves are unlikely to be of much interest to engineers. Nevertheless, it is possible to use the information obtained from a mathematical analysis of software to produce a detailed textual justification of correctness. In this paper, we describe an approach to generating textual explanations from automatically generated proofs of program safety, where the proofs are of compliance with an explicit safety policy that can be varied. Key to this is tracing proof obligations back to the program, and we describe a tool which implements this to certify code auto-generated by AutoBayes and AutoFilter, program synthesis systems under development at the NASA Ames Research Center. Our approach is a step towards combining formal certification with traditional certification methods.
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
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saibi, A., Werner, B.: The Coq proof assistant reference manual: Version 6.1. Technical Report RT-0203 (1997)
Van Baalen, J., Robinson, P., Lowry, M., Pressburger, T.: Explaining synthesized software. In: Redmiles, D.F., Nuseibeh, B. (eds.) Proc. 13th IEEE Conference on Automated Software Engineering, pp. 240–248 (1998)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ (1986)
Coscoy, Y., Kahn, G., Théry, L.: Extracting text from proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 109–123. Springer, Heidelberg (1995)
Denney, E., Fischer, B.: Correctness of source-level safety policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 894–913. Springer, Heidelberg (2003)
Van Deursen, A., Klint, P., Tip, F.: Origin tracking. Journal of Symbolic Computation 15(5/6), 523–545 (1993)
Fischer, B., Schumann, J.: AutoBayes: A system for generating data analysis programs from statistical models. J. Functional Programming 13(3), 483–508 (2003)
Holland-Minkley, A.M., Barzilay, R., Constable, R.L.: Verbalization of high-level formal proofs. In: AAAI/IAAI, pp. 277–284 (1999)
Huang, X.: Proverb: A system explaining machine-found proofs. In: Ram, A., Eiselt, K. (eds.) Proc. 16th Annual Conference of the Cognitive Science Society, Atlanta, USA, pp. 427–432. Lawrence Erlbaum Associates, Mahwah (1994)
Mitchell, J.C.: Foundations for Programming Languages. The MIT Press, Cambridge (1996)
PolySpace Technologies, http://www.polyspace.com
Whittle, J., Van Baalen, J., Schumann, J., Robinson, P., Pressburger, T., Penix, J., Oh, P., Lowry, M., Brat, G.: Amphion/NAV: Deductive synthesis of state estimation software. In: Proc. IEEE Conference on Automated Software Engineering (2001)
Whittle, J., Schumann, J.: Automating the implementation of Kalman filter algorithms. In review (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Denney, E., Venkatesan, R.P. (2004). A Generic Software Safety Document Generator. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-27815-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22381-8
Online ISBN: 978-3-540-27815-3
eBook Packages: Springer Book Archive