Title: Using Formal Proof to meet Executable Object Code and Coverage Objectives in DO-333

Author(s): Colin O’Halloran, Nick Tudor

Publication Event: Proceedings of the Twenty-fifth Safety-Critical Systems Symposium, Bristol, UK

Publication Date: 2017-02-08

Resource URL: https://scsc.uk/r899.pdf

Abstract:

This paper describes a technology proof of concept for the automated verification of Executable Object Code (EOC) using Formal Methods. The project called FEVER was carried out by D-RisQ Ltd in conjunction with Lemma1,both small companies with expertise on various facets of formal verification. The target use of FEVER is within embedded systems that will be require safety certification, specifically targeting unmanned systems. The rationale being that if a route to certification using formal development from requirements to EOC could be shown, then the perceived untenable amount of testing for such systems could be drastically reduced. We chose to use the aerospace software guidance DO-178C, the Formal Methods Supplement DO-333 and Tool Qualification DO-330 as these set out the relevant Objectives for a formal development. The work required the use of a formalised version of the ARM 7 Instruction Set Architecture. This was captured in a language called HOL and was based upon work carried out by Cambridge University. The project used source code for a simple decision making system written in C in order to develop the technology.