Dynamic Analysis for Cyber-Physical Systems

Thursday, 15th May 2014, 10:30 am (SCE Meeting Room)
Speaker: Sridhar Duggirala (University of Illinois Urbana-Champagne)
Title: Dynamic Analysis for Cyber-Physical Systems

Systems that interact with the physical world controlled by instructions from computers are broadly classified as Cyber-Physical Systems (CPS). Such systems are often deployed in safety-critical scenarios, such as avionics, medical devices and automotives. In such scenarios any undesired behavior of the system (commonly called bugs) would lead to catastrophic situations. The complexity of the physical environment, given as nonlinear ODEs and its interaction with software makes the verification problem for such systems very challenging. In this talk, I will explore a technique called Dynamic Analysis for checking whether the safety specification is satisfied by the system.

We consider CPS modeled as a switched nonlinear system provided with user annotations for applying the dynamic analysis technique. These user annotations are a generalization of commonly occurring notions in Control Theory such as Contraction Metric, Incremental Stability and Incremental Forward Completeness. Using these annotations and sample simulations generated by a numerically sound ODE solver, we present an algorithm which gives soundness and relative completeness guarantees for checking safety and temporal precedence properties of these systems. We demonstrate the effectiveness of our approach in two ways. First, we outperform the existing tools for verifying standard nonlinear systems and secondly, we apply our technique for verifying the temporal precedence property of a parallel landing protocol (SAPA) developed by NASA. Our technique could successfully identify the safe operating configurations of the SAPA protocol in the order of minutes.