Workshop on Theorem Proving in Certification

December 5 - 6, 2011, Cambridge, UK

Index of links within this page

        Description of the workshop
                Overview
                Motivating Example
                Format and Schedule
                Organisers

        Additional material added after the workshop


Overview

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
 

Organisers

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