VeriSure: Verification and Assurance

July 14, 2013, Saint Petersburg, Russia

In association with Computer-Aided Verification (CAV) 2013

Introduction

The purpose of the VeriSure Workshop is to explore issues at the conjunction of computer-aided verification and system assurance. In addition to the invited and contributed talks below, there will an open forum for contributions from the floor (5 minutes, 3 slides).

Program

09:00 to 10:30

Robin Bloomfield, Adelard and City University, UK

Invited talk:Reasoning in Safety Cases: Logic and Epistemic

Borzoo Bonakdarpour, U Waterloo, Canada

Gaining Runtime Assurance Through Runtime Verification in Safety-critical Systems

10:30 to 11:00: Coffee

11:00 to 12:30

Hardi Hungar, DLR, Germany

Assuring Standard Conformance of Partial Interfaces

Sebastian Voss, Bernhard Schaetz, Maged Khalil and Carmen Carlan, Fortiss and TUM, Germany

A step towards Modular Certification using integrated model-based Safety Cases

12:30 to 14:00: Lunch

14:00 to 15:30

Vladimir Shelekhov, Ershov Institute, Russia

Validation of Rules for Deductive Verification of Predicate Programs

Martin Hofmann and Harald Ruess, LMU and Fortiss, Germany

Certification for mu-calculus with winning strategies

15:30 to 16:00: Coffee

16:00 to 18:00

Sam Owre, SRI, USA

Building an Assurance Case with The Evidential Tool Bus

Arie Gurfinkel, SEI, USA

Trust in Formal Methods Toolchains

Everyone

Discussion and open forum for 5-minute talks

Workshop Description

The purpose of this workshop is to explore issues at the conjunction of computer-aided verification and system assurance. An autonomous car, for example, must safely negotiate an environment that is imperfectly and incompletely modeled, while using actuators that are themselves imperfect, and guided by fallible sensors whose data requires delicate interpretation and fusion. Assurance here clearly requires more than verification, but can build on verified foundations.

In general, computer-aided verification is usually performed in support of a larger activity whose goal is to provide assurance for a decision with large consequences. The decision may be to send a hardware design for fabrication or to release a commercial software product, in which cases the consequences are economic, or it may be to deploy a system in a context with potential consequences for societal safety or security. In all these cases, verification will be just one of many strands of evidence that contribute to system assurance, and the overall structure of the assurance may be specified or constrained by regulation or certification requirements.

This workshop will explore challenges and opportunities posed for computer-aided verification by the larger context of system assurance. One immediate set of challenges arises from the (recursive) need to provide assurance for the claims delivered by computer-aided verification itself. Related is the challenge of providing assurance for the assumptions and requirements with respect to which the verification is performed. These challenges are situated in pragmatic engineering settings where choices must be made about what should be verified, and to what level of detail, and what should or must be assured by other means (such as testing, human review, or runtime monitoring), and how all these should be combined.

Opportunities arise from the possibility of formalizing and verifying aspects of the larger assurance activity, stimulated by recent proposals that this should be structured as an assurance "case." An assurance case is composed of claims, argument, and evidence, where the argument justifies claims (e.g., for security or safety) based on evidence about the system and its development. An interesting complication is that many top-level claims are probabilistic (e.g., 10^-9 for certain aircraft software) while traditional formal verification is unconditional.

We solicit papers on relevant topics, which include but are not restricted to the following. We encourage exploratory work that will stimulate discussion.

• Quantitative and qualitative assurance claims and arguments
• Integration of formal verification with assurance and with assurance cases
• Modular and incremental methods of verification and assurance
• Toolchains for integrated assurance arguments
• Soundness guarantees for tools, toolchains, and workflows
• Certification and regulatory requirements and standards
• Experience reports and challenges

Workshop Committee

• Jean-Christophe Filliâtre, LRI Université Paris Sud, France
• Mike Gordon, Cambridge University, UK
• Sofia Guerra, Adelard, UK
• Michael Holloway, NASA Langley, USA
• Michaela Huhn, TU-Clausthal, Germany
• Florent Kirchner, CEA, France
• Gerwin Klein, NICTA, Australia
• Tom Maibaum, McMaster University, Canada
• Bertrand Meyer, ETH Zurich, Switzerland
• Grigori Mints, Stanford University, USA
• Harald Ruess, FORTISS, Germany
• Oleg Sokolsky, University of Pennsylvania, USA
• Virginie Wiels, ONERA, France

Important Dates

Note: We kindly ask potential participants to apply for a visa invitation letter as soon as possible (even if their trip plans may change later). For further details please check: CAV Visa page

Application for visa invitation letters supported by CAV (non-EU citizens)	March 20
Application for visa invitation letters supported by CAV (EU citizens)	April 10

Electronic Submissions

Workshop Location

Workshop Organizers