Index of links within this page
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.
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
Additional material added after the workshop