Workshop on Theorem Proving in Certification
December 6 - 7, 2010, Cambridge, UK
Index of links within this page
Description of workshop
Overview
Format and schedule
Organisers
Additional material added after the
workshop
Description of the workshop
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 was 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 was 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.
One lasting outcome of the workshop will be a web page summarising
the results and linking to relevant papers and documents. This web
page, which is derived from
the pre-workshop web page, is a start
at this post-workshop page.
A position paper and a successor workshop are possible additional
results. 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 took place on December 6-7, 2010 in Cambridge, UK IN
the Cormack Room of the University
Centre.
We had a diverse set of participants, representing both the safety and
security assurance communities, who came from organizations including
UK Government, US DoD, Canadian Government, NASA, QinetiQ, Altran
Praxis, ARM, 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
at en.wikipedia.org/wiki/Open
Space Technology. The schedule is below.
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
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
Organisers
The workshop was organised by (in alphabetical order) Naghmeh
Ghafari, Mike Gordon (local arrangements) and Lee Pike. Additional
support was 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.
Additional material added after the
workshop
- Slides of the presentations and the supporting material
- "RTCA DO 178C: An opportunity and challenge for the use of
Theorem-proving in Certification" (Jeff Joyce)
- slides
- accompanied
document
- "Theorem Proving for Certified Mission Assurance" (Shiu-Kai
Chin)
- slides
- "Policy-Based
Design and Verification for Mission Assurance" Chin et al.
- "Credentials
Management for High-Value Transactions" Benson et al.
- "Formal Methods Tool Qualification for DO 178B and DO 178C"
(Nick Tudor)
- "Design by Verification for Safety-Critical Cyber-Physical
Systems" (Pete Manolios)
- "Virtual
Integration of Cyber-Physical Systems by Verification" Manolios et
al.
- "On the Utility of Proof-based Evidence: Experiences from the
Formal Analysis of Fault-Tolerant Systems" (Paul Miner)
- "Revisiting the formal Verification of the Darlington Nuclear
Generating Station Shutdown Systems. 12 Years Later" (Mark Lawford)
- "Automatic Certification and Interactive Theorem Proving: An
Impossible Combination?" (Julien Schmaltz)
- "The Road from Software Testing to Theorem Proving" (Fredric
Painchaud)
- Previous workshops:
- Linking
Tools for Verified Software (2008)
- Interactive
Theorem Proving (ITP) (2009)
- Theory
Engineering: Tools and Practice (2010)
- Trusted
Extensions of Interactive Theorem Provers (2010)
This page last updated by Naghmeh on June 23, 2011.
gipoco.com
is neither affiliated with the authors of this page or responsible
for its contents. This is a safe-cache copy of the original web site.
gipoco.com
is neither affiliated with the authors of this page nor responsible
for its contents. This is a safe-cache copy of the original web site.