Workshop on Theorem Proving in Certification
Cambridge, UK
December 6 - 7, 2010
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 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 will take place on December 6-7, 2010 in Cambridge, UK
at the University
Centre.
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.
The format of the workshop will be a combination of context-setting
presentations together with dynamically-determined discussions during just-in-time sessions. A short description of these
sessions and a set of default discussion topics are given below.
The workshop will be held in the Cormack Room for both days (this is a recent
change). Below is a draft schedule.
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
The workshop schedule includes several sessions reserved for discussion
of impromptu topics that are driven by the interests of participants.
These sessions are based on the "open-space" concept described at http://en.wikipedia.org/wiki/Open
Space Technology.
An initial set of proposed topics for the just-in-time sessions is
shown below. We are looking forward to receiving more suggestions
from other participants between now and the start of the
workshop. Just before lunch on Day 1 of the workshop, we will
open the floor to any last-minute suggestions for session topics, and
then vote to decide which topics will be addressed by dedicated
just-in-time sessions. Each just-in-time session will be assigned
a moderator and someone to record the outcome. Beyond this, what
happens is entirely up to the participants.
The just-in-time sessions are intended to promote real dialogue between
workshop participants and possibly new collaborations. Instead of just
spending all of your time at the workshop listening to prepared
presentations following a preset agenda, the just-in-time sessions will
allow you to engage others in the topics with new thinking,
constructive criticism and problem solving. As organizers, we are
looking forward to being a part of this interaction and tapping into
the knowledge and wisdom about theorem-proving and certification
brought to the workshop by all participants.
A set of default topics for just-in-time sessions:
- "Safety-critical vs. security-critical systems": What are
the commonalities and indomitable differences in theorem-proving for
safety-critical vs. security-critical systems?
- "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?
- "Research effect": What is the greatest 'research' impediment to
the use of theorem-proving in certification today?
- "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?
- "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)?
- "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?
- "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?
- "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)?
- "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
The workshop will be organised by (in alphabetical order) Naghmeh
Ghafari, Mike Gordon (local arrangements) and Lee Pike. Additional
support will be 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.
This page last updated by Mike on December 2, 2010.