Workshop on Theorem Proving in Certification

December 6 - 7, 2010, Cambridge, UK
 

Index of links within this page


 

Description of the workshop

Overview

At least two separate communities - safety and security - are exploring the use of machine-assisted theorem proving (interactive and automatic) as a method for increasing assurance that implementations meet specifications. Certification standards play a role in influencing which methods are used, so it is important to try to ensure that the methods prescribed are effective and practical.

In the security area Common Criteria and FIPS 140 are prominent. In the safety area DO-254 (hardware) and DO-178B (software) are established standards for airborne systems, and DO-178C is being developed to reflect that "current technology trends in software code development are requiring new verification and certification approaches" (a formal methods supplement for DO-178C has been drafted).

The overall goal of the workshop was to consider how formal methods can make systems more reliable, and what value, if any, theorem proving can have in providing assurance. To this end it was hoped to explore synergies between the security and safety critical communities, to contribute to research agendas, and to provide sound arguments that are useful for promoting formal methods and theorem proving.

One lasting outcome of the workshop will be a web page summarising the results and linking to relevant papers and documents. This web page, which is derived from the pre-workshop web page, is a start at this post-workshop page. A position paper and a successor workshop are possible additional results. It is hoped that the results of the workshop will be useful to:

  • procurers and evaluators of systems, who would gain access to arguments for requiring formal proofs;
  • implementers who already use verification by proof, who could use the material to help get their work better understood and valued;
  • certifications standards committee members, who could see the pros and cons for including formal methods;
  • educators, who would get materials to motivate the teaching of formal proof.

Format and schedule

The workshop took place on December 6-7, 2010 in Cambridge, UK IN the Cormack Room of the University Centre. We had a diverse set of participants, representing both the safety and security assurance communities, who came from organizations including UK Government, US DoD, Canadian Government, NASA, QinetiQ, Altran Praxis, ARM, and several academic institutions. The workshop schedule included several sessions reserved for discussion of impromptu topics that were driven by the interests of participants. These sessions were based on the "open-space" concept described at http://en.wikipedia.org/wiki/Open Space Technology. The schedule is below.
Monday, Dec. 6   Presenter/Moderator   Description
------------------- ----------
09:00 - 09:30 Mike, Lee & Naghmeh Welcome: purpose and outcome of the workshop
09:30 - 10:15 Jeff Joyce RTCA DO 178C: An opportunity and challenge
for the use of Theorem-proving in Certification
10:15 - 10:45 Coffee break
10:45 - 11:30 Shiu-Kai Chin Theorem Proving for Certified Mission Assurance
11:30 - 12:00 Jeff Joyce Just-in-time discussion topics
12:00 - 13:30 Lunch
13:30 - 14:00 Nick Tudor Formal Methods Tool Qualification for DO 178B and DO 178C
14:00 - 14:30 Pete Manolios Design by Verification for Safety-Critical
Cyber-Physical Systems
14:30 - 15:45 Just-in-time session
15:45 - 16:15 Afternoon tea
16:15 - 17:30 Just-in-time session

Tuesday, Dec. 7 Presenter/Moderator Description
------------------- -----------
09:00 - 09:30 Paul Miner On the Utility of Proof-based Evidence: Experiences
from the Formal Analysis of Fault-Tolerant Systems
09:30 - 10:15 Mark Lawford Revisiting the Formal Verification of the Darlington
Nuclear Generating Station Shutdown Systems
12 Years Later
10:15 - 10:45 Coffee break
10:45 - 12:00 Just-in-time session
12:00 - 13:30 Lunch
13:30 - 14:00 Julien Schmaltz Automatic certification and Interactive Theorem Proving:
An Impossible Combination?
14:00 - 14:30 Fredric Painchaud The Road from Software Testing to Theorem Proving
14:30 - 15:45 Just-in-time session
15:45 - 16:15 Afternoon tea
16:15 - 17:30 Lee or Naghmeh Wrap-up and workshop outcome planning

Organisers

The workshop was organised by (in alphabetical order) Naghmeh Ghafari, Mike Gordon (local arrangements) and Lee Pike. Additional support was provided by Joe Hurd and Jeff Joyce. Naghmeh and Jeff are from Critical Systems Labs (CSL), Lee and Joe are from Galois and Mike is from the University of Cambridge Computer Laboratory.

 


Additional material added after the workshop

  • Slides of the presentations and the supporting material
    • "RTCA DO 178C: An opportunity and challenge for the use of Theorem-proving in Certification" (Jeff Joyce)
    • "Formal Methods Tool Qualification for DO 178B and DO 178C" (Nick Tudor)
    • "On the Utility of Proof-based Evidence: Experiences from the Formal Analysis of Fault-Tolerant Systems" (Paul Miner)
    • "Revisiting the formal Verification of the Darlington Nuclear Generating Station Shutdown Systems. 12 Years Later" (Mark Lawford)
    • "Automatic Certification and Interactive Theorem Proving: An Impossible Combination?" (Julien Schmaltz)
    • "The Road from Software Testing to Theorem Proving" (Fredric Painchaud)


 

This page last updated by Naghmeh on January 25, 2011.
Comments