CPS V&V I&F Workshop 2014: Talks

Table of Contents
  1. Aerospace Challenges
    1. Kristin Y. Rozier: Integration of Formal Methods into Design and Implementation of Aerospace
    2. Jean-Baptiste Jeannin: Challenges in the Verification of Existing Aerospace Systems
    3. Alwyn Goodloe: Challenges in the Verification of Flight-Critical Systems
  2. Automotive Challenges
    1. Jim Kapinski: Ongoing Challenges in Applying V&V Technologies to Automotive Engine Control
    2. Thomas Heinz: Hybrid Systems Verification Challenges at Bosch
  3. Modeling
    1. David Garlan: Multi-domain Modeling of Cyber-Physical Systems using Architectural Views
    2. Dionisio de Niz: Analysis Contracts for CPS
  4. Analysis
    1. André Platzer: Logical Foundations of Cyber-Physical Systems
    2. Ian Mitchell: Scalable Parametric Approximations of the Maximal Controlled Invariant Set and Two Health Related Application Domains
    3. Khalil Ghorbal: Reasoning About Dynamical Systems Using Invariants: Achievements and Challenges
    4. Sriram Sankaranarayanan: Deductive Approaches for Stochastic Systems
  5. Synthesis
    1. Sicun Gao: Nonlinear Control as Program Synthesis
  6. Bridging
    1. Taylor Johnson: Cyber-Physical Specification Mismatch Identification with Dynamic Analysis Systems
    2. Stefan Mitsch: Verified runtime validation of verified cyber-physical system models
    3. Parasara Sridhar Duggirala: Simulations to Proofs in C2E2

Aerospace Challenges

Kristin Y. Rozier: Integration of Formal Methods into Design and Implementation of Aerospace

The value of formal methods in aerospace system design and verification has been demonstrated increasingly frequently, leading to more widespread acknowledgment of the essentialness of incorporating these methods into any safety-critical project. However, the success stories have mainly demonstrated the value of the results of formal methods analysis, advancing formal techniques in terms of scalability, efficiency, and adaptability to the range of complex problems in the aerospace domain. While this has gone a long way to winning over the perception of formal methods as a valuable and integral tool, it has not addressed some of the most significant bottlenecks in the process and the original barriers to adaptation. These challenges include creating a formal model and extracting formal specifications from a development process that might never before have created them. This talk will briefly survey the successes and highlight the remaining barriers to adaptation of formal methods in aerospace. Unless we address these challenges in the near future, the progress of formal methods in aerospace may be stalled.
[slides]

Jean-Baptiste Jeannin: Challenges in the Verification of Existing Aerospace Systems

Formal methods are being used successfully to verify more and more aerospace systems, including fly-by-wire, avionics and collision avoidance systems. Verification is often easier when done jointly with design; in practice however, one often has to verify existing systems, or already-designed system, with little or no possible input into the design. As a result, the verification is often done on an idealized model of the system, typically designed by the verification team, rather than on the system that will actually run. In those circumstances, how do we bridge the gap between the verified system and the running system? Additionally, a number of challenges arise when making the verified system more realistic. Uncertainty is everywhere: wind changes the trajectory of aircraft, sensors give the system a view of the world with limited precision, and humans can sometimes react in difficult-to-predict manners. Moreover, a computer system uses floats with limited precision, and it is necessary to analyze the possible rounding errors. Finally, to make verification scalable to complex aerospace systems, proof automation is crucial.
[slides]

Alwyn Goodloe: Challenges in the Verification of Flight-Critical Systems

This talk is intended to stimulate discussion on some of the issues surrounding formal verification. We first give a very brief introduction to the issues of verification in the context of certification of software in civil aviation. We will then address challenges in applying formal methods in the context of safety-critical systems and challenges posed by the current certification regime. We will also discuss challengers posed as the cockpit becomes highly automated by full autonomy.
[slides]

Automotive Challenges

Jim Kapinski: Ongoing Challenges in Applying V&V Technologies to Automotive Engine Control

In the model-based development (MBD) paradigm for embedded control software, verification and validation (V&V) technologies are critical to ensure high quality of the software. In the automotive context, powertrain control (PTC) software development is increasingly being performed using MBD principles; however, application of advanced V&V techniques to PTC software continues to be a difficult task. We present some key features of PTC systems that contribute to this challenge and discuss our perspective on the spectrum of extant V&V techniques. We argue that simulation-based techniques to increase confidence in system designs should be investigated, and we present an overview of some of our recent work in this space.
[slides]

Thomas Heinz: Hybrid Systems Verification Challenges at Bosch

This talk gives an overview of some important verification challenges automotive industry in general and Bosch in particular face today and in the near future. The challenges are mostly driven by the need of technology to realize safe automated driving and robotics applications involving human interaction. Recently, an European publicly funded project (UnCoVerCPS - Unifying Control and Verification of Cyber-Physical Systems) has been approved which addresses these problems using a combination of offline and online verification techniques. In order to leverage formal verification in the development of novel safety critical applications, it is crucial to ensure that properties proven on abstract continuous/hybrid models still hold in the actual implementation. Finally, to address modular development of control functions, the notion of a safe interface is introduced which guarantees that a specified safety property holds for a hierarchical control design under arbitrary input.
[slides]

Modeling

David Garlan: Multi-domain Modeling of Cyber-Physical Systems using Architectural Views

Today's complex cyber-physical systems require the use of a variety of models to capture different aspects of these systems: physical models, software models, control models, and so on. A critical challenge is to ensure consistency and completeness of these models. In this talk we describe an approach that uses architectural models as the basis for reconciliation. Specifically, a base architecture of the system is used as a unifying representation to compare the structure and semantics of the associated models through a set of architectural projections, or views. Each model is related to the base architecture through the abstraction of a corresponding architectural view, which captures structural and semantic correspondences between model elements and system entities. The use of the architectural view framework to relate system models from different domains is illustrated in the context of a quad-rotor air vehicle and on-going collaborations with Toyota and the Software Engineering Institute.
[slides]

Dionisio de Niz: Analysis Contracts for CPS

Developing cyber-physical systems involves multiple engineering domains, e.g., timing, logical correctness, thermal resilience, and mechanical stress. In today's industrial practice, these domains rely on multiple analyses to obtain and verify critical system properties. Domain differences make the analyses abstract away interactions among themselves, potentially invalidating the results. Specifically, one challenge is to ensure that an analysis is never applied to a model that violates the assumptions of the analysis. Since such violation can originate from the updating of the model by another analysis, analyses must be executed in the correct order. Another challenge is to apply diverse analyses soundly and scalably over models of realistic complexity. To address these challenges, we develop an analysis integration approach that uses contracts to specify dependencies between analyses, determine their correct orders of application, and specify and verify applicability conditions in multiple domains. We implement our approach and demonstrate its effectiveness, scalability, and extensibility through a verification case study for thread and battery cell scheduling.
[slides]

Analysis

André Platzer: Logical Foundations of Cyber-Physical Systems

This talk briefly surveys the logical foundations of cyber-physical systems and how they manifest in differential dynamic logics for multi-dynamical systems. Multi-dynamical systems are a mathematical model for CPS, characterizing them by combining multiple facets of dynamical systems, including discrete and continuous dynamics, but also uncertainty resolved by nondeterministic, stochastic, and adversarial dynamics. Multi-dynamical systems help us understand CPSs better, as being composed of multiple dynamical aspects, each of which is simpler than the full system. Differential dynamic logics exploit this compositionality in order to tame the complexity of CPS.

After a brief survey, this talk gives a criticial assessment of the applications of differential dynamic logics, emphasizing why and when the approach works particularly successfully and what technical aspects make an application challenging. The talk concludes by identifing the most important unsolved challenges that are holding back the CPS V&V community.
[slides]

Ian Mitchell: Scalable Parametric Approximations of the Maximal Controlled Invariant Set and Two Health Related Application Domains

I present a connection between the viability kernel (or maximal controlled invariant set) and maximal reachable sets, which allows scalable parametric approximations of the latter to be used to conservatively compute the former. This general algorithm has been implemented with two specific parametric representations: one is more accurate, scalable and tunable, while the other has been extended to robust approximations, continuous time and sampled data models and synthesis of control signals which guarantee safety. I then consider two health application domains where safety analysis is desirable: feedback control of anesthesia and collision avoidance in smart wheelchairs. In one case progress has been made and in the other, well, no so much...
[slides]

Khalil Ghorbal: Reasoning About Dynamical Systems Using Invariants: Achievements and Challenges

During this talk, I will briefly review, from a computer science perspective, the definitions and use of invariants for dynamical systems modeled by ordinary differential equations. From there, I will present recent related results as well as the fundamental and technical challenges we are facing to push further the automated reasoning about invariants. I will also try to motivate the need for a common representative set of benchmarks to compare the currently available techniques as well as their future improvements.
[slides]

Sriram Sankaranarayanan: Deductive Approaches for Stochastic Systems

In this talk, we will address the problem of analyzing stochastic systems to place bounds on the probabilities of property failures. We present the use of Martingales and concentration of measure inequalities as fundamental tools for reasoning about stochastic systems and discuss open problems in this space.
[slides]

Synthesis

Sicun Gao: Nonlinear Control as Program Synthesis

I will show how program synthesis and automated reasoning techniques can provide a new framework for automated and reliable controller design for nonlinear and hybrid systems.
[slides]

Bridging

Taylor Johnson: Cyber-Physical Specification Mismatch Identification with Dynamic Analysis Systems

Embedded systems use increasingly complex software and are evolving into cyber-physical systems (CPS) with sophisticated interaction and coupling between physical and computational processes. Many CPS operate in safety-critical environments and have stringent certification, reliability, and correctness requirements. These systems often undergo changes throughout their lifetimes, where the software, physical hardware, and environmental assumptions are updated in subsequent design iterations. One source of failure in safety-critical CPS is when there are unstated assumptions in either the physical or the cyber parts of the system, and new or updated components do not match those assumptions. In this talk, we present an automated method towards identifying unstated assumptions in CPS. Dynamic specifications in the form of candidate invariants of both the software and physical components are identified using dynamic analysis (executing and/or simulating the system implementation or model thereof). A prototype tool called Hynger (for HYbrid iNvariant GEneratoR) was developed that instruments Simulink/Stateflow (SLSF) model diagrams to generate traces in the input format compatible with the Daikon invariant inference tool, which has been extensively applied to software systems. Hynger, in conjunction with Daikon, is able to detect candidate invariants of several CPS case studies. We use the running example of a DC-to-DC power converter, and demonstrate that Hynger can detect a specification mismatch where a tolerance assumed by the software is violated due to a plant change. More broadly, we highlight CPS challenges arising due to increasingly sophisticated software used to control physics, and highlight software engineering techniques that may help enable reliable CPS.
[slides]

Stefan Mitsch: Verified runtime validation of verified cyber-physical system models

Formal verification and validation play a crucial role in making cyberphysical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This talk discusses how offline verification results of CPS models can be combined with runtime validation of system executions for compliance with the model, and highlights the current and future challenges linked to runtime validation of CPS.
[slides]

Parasara Sridhar Duggirala: Simulations to Proofs in C2E2

Simulations are a scalable way for testing complex Cyber-Physical Systems. However, proving formal properties using simulations has proved to be challenging. In this talk I present an approch for formally proving properties of hybrid systems using simulations and annotations. These annotations, called discrepancy functions, are extensions of well studied convergence and divergence metrics in Control Theory. To demonstrate the scalability of this approach, I present two case studies. First, is verifying temporal properties of an alerting system for a parallel landing protocol. Second, uses extension of discrepancy functions to analyze network of cardiac cells. I will also present the future challenges in extending the approaches to compositional verification and synthesis.
[slides]