Workshop on High-Consequence Control Verification
July 18, 2016
Bahen Centre for Information Technology
University of Toronto
Toronto, Ontario, Canada
In conjunction with the 28th International Conference on Computer Aided Verification.
| 09:00‑09:05 | Opening |
| Session 1: Cyber-Physical Design (Chair: Jackson R. Mayo) | |
| 09:05-10:00 | Sanjit A. Seshia (UC Berkeley) Invited Presentation Formal Inductive Synthesis for Cyber-Physical Systems (abstract) |
| 10:00-10:30 | Lee Pike (Galois, Inc.) Hints for High-Assurance Cyber-Physical System Design (abstract) |
| 10:30-11:00 | Break |
| Session 2: Digital Refinement (Chair: Karthik V. Aadithya) | |
| 11:00-11:40 | Karla Morris (Sandia) and Colin Snook (University of Southampton) Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics (paper) |
| 11:40-12:10 | Philip Johnson-Freyd (University of Oregon) The “Push-Out” Approach to Refinement and Composition for High-Consequence Systems (abstract) |
| 12:10-01:50 | Lunch (attendees on their own) |
| Session 3: Continuous Variables (Chair: Karla Morris) | |
| 01:50-02:20 | Michael Butler (University of Southampton) and Toby Wilkinson (University of Southampton) Formal Development of Supervision for Autonomous Systems (abstract) |
| 02:20-02:50 | Sylvie Boldo (Inria) Iterators: Where Folds Fail (abstract) |
| 02:50-03:20 | Karthik V. Aadithya (Sandia), Baruch Sterin (UC Berkeley), Sayak Ray (Intel Corporation), Pierluigi Nuzzo (UC Berkeley), Alan Mishchenko (UC Berkeley), Robert Brayton (UC Berkeley), and Jaijeet Roychowdhury (UC Berkeley) ABCD: Accurate Booleanization of Continuous Dynamics for Analog/Mixed-Signal Design and Verification (abstract) |
| 03:20-03:25 | Closing |
Scope
The Workshop on High-Consequence Control Verification (HCCV) focuses on formal methods concepts and techniques to ensure the highest levels of reliability, safety, and security for digitally controlled devices, including the effects of possibly extreme physical environments. The workshop targets applications where the severe consequences of failure justify extraordinary investments not appropriate for less critical devices – including special methodologies at the design stage to enable verifying stringent reliability, safety, and security requirements in the resulting devices under both nominal and out-of-nominal (fault) conditions. Such needs exist in domains including defense, medical devices, and scientific instrumentation.
The willingness to make greater investments for small but high-consequence devices can provide an opportunity to leverage emerging, more powerful formal methods techniques that may currently be considered too costly for “mainstream” industrial applications. Novel ideas for design and analysis techniques that promote in-depth verifiability are of strong interest for these high-consequence digital controllers. The HCCV workshop offers a new forum for engagement among formal methods researchers, tool developers, and practitioners.
Topics of interest include:
- Theory and techniques for formally verified high-consequence digital design (via model checking and/or theorem proving), such as:
- Abstraction/refinement
- Correct-by-construction synthesis
- Exhaustive or probabilistic analysis of fault consequences
- Incorporation of analog physics
- Applications to safety-critical digitally controlled devices in domains such as:
- Defense
- Medical
- Supervisory control and data acquisition (SCADA)
Organizers
Jackson R. Mayo (co-chair)
Sandia National Laboratories
Livermore, California, United States
jmayo@sandia.gov
Michael J. Butler (co-chair)
University of Southampton, United Kingdom
mjb@ecs.soton.ac.uk
Program Committee
- Richard Banach (University of Manchester)
- Sylvie Boldo (Inria)
- Marco Bozzano (Fondazione Bruno Kessler)
- Robert Clay (Sandia)
- Neil Evans (Atomic Weapons Establishment)
- Sumit Kumar Jha (University of Central Florida)
- David Monniaux (VERIMAG)
- Karla Morris (Sandia)
- Peter Ölveczky (University of Oslo)
- Karem Sakallah (University of Michigan)
- Mariëlle Stoelinga (University of Twente)