A Generic Software Safety Document Generator

13 years 10 months ago

Download ti.arc.nasa.gov

Abstract. Formal certiﬁcation is based on the idea that a mathematical proof of some property of a piece of software can be regarded as a certiﬁcate 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 justiﬁcation 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 certiﬁcat...

Ewen Denney, Ram Prasad Venkatesan

Real-time Traffic