Workshop on Theorem Proving in Certification

December 5 - 6, 2011, Cambridge, UK

Index of links within this page

        Description of the workshop
                Motivating Example
                Format and Schedule

        Additional material added after the workshop


This workshop was a follow-on workshop to the one that took place on December 6-7 in Cambridge last year. For more information about the motivation behind this workshop please refer to the 2010 webpage. The general theme of the 2011 workshop was on developing "next generation" formal methods assurance cases with a focus on theorem proving.

The aim was to bring together participants from both the safety and security assurance communities to share experiences and discuss common problems. The majority of participants were familiar with some theorem proving technology and wanted to see its role in critical systems better appreciated. In addition, we had a number of observers who were less expert technically, but were interested in the area and contributed to the general discussions.

Motivating Example

To stimulate and unify the discussions, we developed a common example that was addressed by the speakers and participants. Here is a sample pseudo code that implements the functions described in the example. Please note that the pseudo code has not been compiled or checked in any way by a software tool. The code has been seeded intentionally with a few defects and other aberrations (just to make it interesting!). The required behavior is specified on the first page of the pseudo code along with assumptions.

We encouraged the participants to approach this example from various angles and varying levels (e.g., actual code vs. formal model vs. assurance case).

This example involves a variety of different kinds of complexities which are an opportunity to demonstrate the flexibility of a theorem proving approach, e.g., reasoning about timing relationships, arithmetic calculations, and non-trivial decision logic.

A preliminary list of questions and comments which were addressed by the participants in the context of this example is given below.
In addition, we prepared a simplified "certification standard" that participants referred to when explaining how their approach might be used to support the overall objectives of certification.

Format and Schedule

The workshop took place on December 5-6, 2011 in Cambridge, UK at the Computer Laboratory (William Gates Building) in room SW01. We had a diverse set of participants, representing both the safety and security assurance communities, who came from organizations including UK Government, US Government, NRL, QinetiQ, Altran Praxis, Ada Core, Rolls Royce, Critical Software 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 here. The schedule is below.

Monday, Dec. 5   Presenter/Moderator   Description
------------------- ----------
09:00 - 09:30 Naghmeh Welcome: purpose of the workshop
09:30 - 10:15 Duncan Brown ED-218, The Formal Methods Supplement for ED-12C(DO-178C)
10:15 - 10:45 Coffee break
10:45 - 12:00 Naghmeh and Jeff Discussion of the example
12:00 - 13:30 Lunch
13:30 - 14:15 Rod Chapman Implementation and Analysis of the Nose-Gear
Velocity example in SPARK
14:15 - 15:00 John Hatcliff Using Symbolic Execution to Obtain Greater Automation and
Flexibility for Checking Spark Software
Contracts in Critical Embedded Systems
15:00 - 15:30 Afternoon tea
15:30 - 16:15 Paul Curzon Safe Assurance Cases, Proof and the Prevention of User Error
16:15 - 16:45 Just-in-time session discussion topics
16:45 - 17:30 Duncan Brown Tamarack standard Discussion (objectives K/L/T)

19:00 - 21:00 Workshop Dinner: menu (three courses provided, but you may have to pay for your drinks)

Tuesday, Dec. 6 Presenter/Moderator Description
------------------- -----------
09:00 - 09:45 Elizabeth Leonard Middle Men: Obligations and Needs of the
Certification Team
09:45 - 10:15 Colin O'Halloran Nose Gear Velocity Challenge, A Sketch of an Approach
10:15 - 10:45 Coffee break
10:45 - 12:00 Lee Nose Gear Breakout Session
12:00 - 13:30 Lunch
13:30 - 14:15 Yannick Moy Integrating Formal Program Verification with Testing
14:15 - 15:00 Tamarack standard Discussion (objectives U/V/W)
15:00 - 15:30 Afternoon tea
15:30 - 16:45 Just-in-time session
16:45 - 17:00 Lee Wrap-up and workshop outcome planning


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

Additional material added after the workshop

Below are the slides of some the presentations:

This page last updated on January 10th, 2012 by Naghmeh.
(Tested by Mike on Feb 20, 2012.)