Toward a cooperative and open framework for the development of certifiable software

On December 5-6, I participated in the 2nd workshop on Theorem Proving in Certification, in Cambridge (UK). This turned out to be even more interesting than last year’s program promised.

The goal of the workshop is to clarify under which conditions theorem proving can be applied in the context of DO-178C Formal Methods Supplement (hence Prove & Fly!):

• extent of verifications performed
• cost/benefit compared to testing
• characteristics of a technique/tool to be called theorem proving
• tool qualification needs

The workshop was organized around a common challenge (gear nose challenge) which all participants were invited to address from different angles. The challenge was to compute the velocity of the nose gear of a plane while on the ground. This was made even more interesting by the need to comply with a small certification standard (Tamarack standard). Both the challenge and the certification standard were created by Jeff Joyce from CSL.

Besides sharing the strategy we follow in project Hi-Lite, and showing how it applied to the common challenge, I was very interested in the discussions we had over tool qualification and the alternate objectives to coverage in DO-178C, when using formal verification instead of testing. An interesting shared opinion was that the automatic prover does not need to be qualified if it generates a trace that can be double-checked independently by a theorem prover (based on a small set of induction rules). For example, that’s the case for CVC3. In the discussion on alternate objectives to coverage, Jeff Joyce clearly stated that the underlying goal is to detect incompleteness of specifications, or equivalently (from the opposite point of view) unintended functionalities. During the discussion, it appeared that we may be able to use either model checking to perform a symbolic coverage analysis, or information given by automatic provers stating which hypotheses (and thus source code constructs) were used in proofs, but for example not concolic testing which is based on source code.

Many of these subjects will need to be further explored as DO-178C is adopted in new projects and tools based on formal methods are applied in this context. In particular, I look forward to the evolutions of the Tamarack standard and new solutions to the gear nose challenge. Hot news: Open-DO will host the workshop forge and wiki to support these evolutions.