CPS V&V I&F Workshop 2016: Talks

Table of Contents
  1. Aerospace Session
    1. Alwyn E. Goodloe: Challenges to Applying AI in Safety-Critical Systems
    2. Kristin Y. Rozier: Specification: The Biggest Bottleneck in Aerospace V&V and Autonomy
  2. Solutions I
    1. Nathan Fulton: The KeYmaera X Theorem Prover
    2. Sriram Sankaranarayanan: Switched Stabilization of Polynomial Dynamical Systems
    3. Sarah Loos: Differential Refinement Logic
  3. Car and Ground Robot Session
    1. Jim Kapinski: Challenges in applying V&V technologies to automotive cyber-physical systems
    2. Shahab Kaynama: Real-Time Safety Guarantees in Robotics: Challenges and Limitations
  4. Solutions Session II
    1. Mo Chen: Some Recent Advances in Hamilton-Jacobi Reachability Theory and Applications
    2. Jie Fu: Scalable temporal logic synthesis for cyber-physical systems
    3. Antonio Iannopollo, Marten Lohstroh: Adaptive Contracts for the Internet of Things
    4. Akshay Rajhans: Recent Advancements in MathWorks Verification and Validation Tools and Techniques

Aerospace Session

Alwyn E. Goodloe: Challenges to Applying AI in Safety-Critical Systems

Safety-Critical cyber-physical systems (CPS), such as aircraft and automobiles, are those systems whose failure could result in loss of life, significant property damage, or damage to the environment. The grave consequences of failure have compelled industry and regulatory authorities to adopt conservative design approaches and exhaustive verification and validation (V&V) procedures to prevent mishaps. Yet advances in artificial intelligence (AI) are enabling the development of increasingly autonomous (IA) CPS that modify their behavior in response to the external environment and learn from their experience. In this talk, we will discuss cultural, regulatory, and, technological impediments to applying AI in safety-critical CPS. The talk will emphasize the challenges of verification and validation of such systems especially within existing regulatory frameworks.

Kristin Y. Rozier: Specification: The Biggest Bottleneck in Aerospace V&V and Autonomy

The advent of increasingly AI-enhanced control in autonomous systems stands on the shoulders of formal methods, which make possible the rigorous safety analysis autonomous systems require. For example, an aircraft cannot operate autonomously unless it has design-time reasoning to ensure correct operation of the autopilot and runtime reasoning to ensure system health management, or the ability to detect and respond to off-nominal situations that could not be verified at design time. Formal methods are highly dependent on the specifications over which they reason; not only are specifications required for analysis, but there is no escaping the "garbage in, garbage out" reality. Correct, covering, and formal specifications are thus an essential element for enabling autonomy. However, specification is difficult, unglamorous, and arguably the biggest bottleneck facing verification and validation of aerospace, and other, autonomous systems. This talk will examine the outlook for the practice of formal specification, and highlight the on-going challenges of specification, from design-time to runtime system health management. We will pose challenge questions for specification that will shape both the future of formal methods, and our ability to more automatically verify and validate autonomous systems of greater variety and scale.
[ slides ]

Solutions I

Nathan Fulton: The KeYmaera X Theorem Prover

KeYmaera X is an automated theorem prover for hybrid systems. A small trusted prover core (~1700 lines) isolates all code that could result in the prover concluding a system is safe when in fact the system is not safe. A large library of tactics built on top of this core enables proof search procedures that aim to simplify verification of large and complicated hybrid systems models. This talk will present the main features of KeYmaera X that differentiate it from existing hybrid system analysis tools (including its predecessor KeYmaera) and will discuss limitations that ongoing KeYmaera X development efforts are addressing.
[ slides ]

Sriram Sankaranarayanan: Switched Stabilization of Polynomial Dynamical Systems

We consider the problem of automatically synthesizing region stabilizing controllers for polynomial dynamical systems. The goal of our synthesis is to produce switching controllers that can switch between finitely many modes to ensure that the resulting closed loop dynamics are guaranteed to reach a given small target region around the equilibrium (and stay there). Our approach uses the notion of a control Lyapunov function, an extension to standard Lyapunov functions for non-autonomous (controlled) systems. We show that a relatively simple modification to the standard control Lyapunov formulation works for the switched system case, and yields controllers with guaranteed minimum dwell times, that can be implemented inside a computer. Next, we present schemes for automatically discovering control Lyapunov functions by reducing the problem to solving a system of quantified constraints over the reals. We examine the solution of these constraints using a procedure called Counter-Example Guided Inductive Synthesis (CEGIS) driven by nonlinear delta-satisfiability solvers such as dReal, or through a Linear Matrix Inequality (LMI) relaxation of the nonlinear constraints.

Sarah Loos: Differential Refinement Logic

Differential refinement logic (dRL) us a logic with first-class support for refinement relations on hybrid systems, and a proof calculus for verifying such relations. It simultaneously solves several seemingly different challenges common in theorem proving for hybrid systems: 1) When hybrid systems are complicated, it is useful to prove properties about simpler and related subsystems before tackling the system as a whole. 2) Some models of hybrid systems can be implementation-specific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed. 3) One approach to taming the complexities of hybrid systems is to start with a simplified version of the system and iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof. 4) When proofs become large, it is difficult to maintain a modular or comprehensible proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability and modularity of the resulting proof.

Car and Ground Robot Session

Jim Kapinski: Challenges in applying V&V technologies to automotive cyber-physical systems

Embedded control system designs are used in many cyber-physical systems (CPSs) applications, such as automotive engine control systems. Many of these applications have critical requirements, so it is vital to ensure correctness of the designs; however, verification and validation (V&V) for industrial CPS designs remains a difficult and expensive process. This talk presents an overview of V&V techniques currently used for industrial CPS applications and presents challenges in applying new approaches to applications in the automotive domain.

Shahab Kaynama: Real-Time Safety Guarantees in Robotics: Challenges and Limitations

In unstructured, uncertain, highly dynamic environments self-driving vehicles face a challenging task: how to formally guarantee safety beyond what the bare standards and regulations dictate, while not sacrificing performance. Indoor robotics for materials transport and handling is no exception. With the recent widespread emergence of Industry 4.0, Clearpath is leading the way in deploying fleets of infrastructure free, locally connected, self-driving vehicles in highly dynamic factory floors with heavy, somewhat chaotic traffic, tight navigable spaces and stringent takt times. In this short talk we will overview the challenges involved with guaranteeing safety of cyberphysical systems in real time under non-trivial constraints. We will discuss open fundamental and computational problems in an attempt to bridge the gap between industrial needs and academic research.

Solutions Session II

Mo Chen: Some Recent Advances in Hamilton-Jacobi Reachability Theory and Applications

Recently, there has been an immense surge of interest in using unmanned aerial vehicles (UAVs) for civilian applications. These applications include package delivery, fire fighting, aerial surveillance, and fast disaster response. As a result, UAV traffic management (UTM) systems are needed to support potentially thousands of UAVs flying simultaneously in the airspace, in order to ensure that the liveness and safety requirements of UAVs are met. Hamilton-Jacobi (HJ) reachability is a powerful tool for guaranteeing the liveness and safety of nonlinear and hybrid systems such as UAVs, and involves computing the reachable set, which is roughly the set of states from which a system can be driven to a certain pre-specified set of states. However, in HJ reachability, computing the reachable set involves solving a partial differential equation on a grid that represents the discretization of the state space. This makes the computation complexity scale exponentially with the number of states, and limits the application HJ reachability to systems with approximately 5 or fewer continuous state dimensions. ​​To alleviate limitations due to computation complexity, several techniques have been developed to either compute exactly or approximate the reachable set for systems with special properties, such as having terminal integrators or having weakly coupled structure. For systems without the required properties, approximations can be made to simplify the system so that approximate reachable sets can be efficiently computed.

Jie Fu: Scalable temporal logic synthesis for cyber-physical systems

Formal synthesis provides provably correct controllers for systems constrained by complex temporal logic specifications. However, the issue of scalability hinders their applications to large-scale cyber-physical systems. In this talk, I will present two scalable synthesis algorithms to attack this issue. These methods are suitable for optimal control design and verification in large-scale systems. In particular, the first approach leverages distributed optimization for formal control design. It exploits the modularity and loose-coupling between subsystems in a large-scale stochastic cyber-physical system and enables parallel synthesis. The second one incorporates approximate dynamic programming and hybrid system theory for scalable temporal-logic constrained control design.

Antonio Iannopollo, Marten Lohstroh: Adaptive Contracts for the Internet of Things

Well-vetted methodologies that over the past several decades have proven quite effective in semiconductor design and have been a determining factor in the upholding of Moore’s Law, break down in the face of the continuously and rapidly evolving character of the Internet of Things. The IoT is envisioned to be a widely distributed, interconnected, and heterogeneous system of systems that is able to operate in hostile, unpredictable conditions. Vast heterogeneity, ever-changing environment assumptions, and the inability to pin down the utility of a component exclusively at design time pose significant challenges to achieving this goal. In this talk, we introduce the idea of "adaptive contracts," which cast run-time dynamic re-configuration and re-purposing into a formal framework, providing the first steps toward a disciplined design methodology for the IoT.
[ slides ]

Akshay Rajhans: Recent Advancements in MathWorks Verification and Validation Tools and Techniques

This solution talk presents some recent advancements in verification and validation capabilities in MathWorks tools and their applications to the CPS domain. New model metrics for measuring model complexity assist in improving the readability and portability of Simulink models. Model slicing enables the isolation of problematic behavior in large and complex models by slicing the model to only the relevant blocks for given operating conditions and time windows of interest. Our Polyspace static code analysis products can now check C/C++ code for standards compliance (such as the MISRA-2012 standard). The Polyspace Bug Finder now has a vast array of security-focused checks for security, tainted data and concurrency. Auto-generation of tests for C code in S-functions is now facilitated by Simulink Design Verifier, and code-coverage reports from Simulink Verification & Validation allow the user to confirm adequate test coverage. We will show how these new capabilities help automate and streamline critical software design and development in context of the V-model. We will conclude the talk by outlining research and development challenges in this domain.