Workshop on Theorem Proving in Certification

Overview

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 is 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 is 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.

The aim is to bring together participants from both the safety and security assurance communities to share experiences and discuss common problems. We hope that the majority of participants will have familiarity with some theorem proving technology and would like to see its role in critical systems better appreciated. In addition, we hope to have a number of observers who might be less expert technically, but who are interested in the area and can contribute to the general discussions.

A lasting outcome of the workshop would be a web page summarising its results and linking to relevant papers and documents. A post workshop position paper is a possible additional result. 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 is free, but participants will need to make their own travel and accommodation arrangements.

Some hotel information can be found on this map and at Hotels Combined. There is a direct bus from Heathrow Airport to Cambridge (possibly obsolete timetable) or several very convenient, but very expensive, taxi services (Microsoft and the Computer Laboratory often use ECS). Stansted Airport is about 30 minutes drive from Cambridge and there are buses, taxis and a trains available in the airport terminal.

We have invited a fairly diverse audience (from both academic and industry).  We have 27 confirmed participants from different organizations including UK Government, US DoD, Canadian Government, NASA, QinetiQ, Altran Praxis, ARM, and several academic institutions.

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

 19:00 - 21:00   Dinner (£30, menu)
 [Please email Mike with starter and main course selection if you wish to attend]

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

1. "Safety-critical vs. security-critical systems":  What are the commonalities and indomitable differences in theorem-proving for safety-critical vs. security-critical systems?
2. "Future of interactive theorem-proving":  What will interactive theorem-proving be like (in terms of technology, pervasiveness of use, etc.) in 5, 20, and 50 years?  Why will it remain relevant?
3. "Research effect": What is the greatest 'research' impediment to the use of theorem-proving in certification today?
4. "Conservative Representation":  How is it possible to demonstrate that a formal representation is a 'conservative representation' (as defined in the formal methods supplement of  DO 178C) of some behavior?
5. "Necessary Requirements":  How is it possible to demonstrate, using theorem-proving, that every 'low level software requirement' is necessary with respect to the 'high level software requirements' (as per the formal methods supplement of DO 178C)?
6. "Avoidance of Unintended Functionality":  How can theorem-proving be used to detect if the implementation of a software system contains functionality which is not necessary to satisfy the functional requirements?
7. "As good as MCDC Structural Coverage":  What must be achieved by a theorem-proving approach to claim that the verification of a software system is at least as "good as" a conventional test-based approach that achieves MCDC structural coverage?
8. "Soundness of a Theorem-proving Approach":  What, in practical terms, is the minimum that must required of a theorem-proving approach to satisfy the requirement of the DO 178C formal methods supplement that the soundness of a formal method must be demonstrated (if the formal methods is used to produce verification results for certification credit)?
9. "Assurance Cases":  What is the greatest 'value-add' of interactive theorem-proving to developing an assurance case? If verification results obtained by means of theorem-proving are to be submitted for certification credit (in place of conventional test based results), what needs to be included in the package of results submitted to the certification authorities, i.e., what in addition to "theorem proved" is needed?

Organisation