Project Summary Collaborative: CNS: Small: Rigorous Verification and Synthesis for Cyber-Physical Systems from Simulations PIs: G. Fainekos and S. Sankaranarayanan Verification and synthesis approaches for hybrid, cyber-physical systems (CPS) are proposed. The proposed approaches will use extensive simulations to verify and synthesize controllers for safety and stability properties. Existing approaches to verification and correct-by-construction synthesis are mostly symbolic, using exhaustive search over the state (and action) space, guided by decision procedures. However, the existing state-of-the-art symbolic techniques are inadequate in many practical applications. The primary challenge in these applications lies in the complexity of the physics of the system modeled as non-linear ODEs with a large number of state variables. In some cases, these models are not available in a closed form symbolic representation suitable for symbolic approaches. To address these challenges, we propose a new class of techniques centered on the ability to simulate systems and the availability of simpler approximate models of the system dynamics to combine concrete and symbolic exploration. The main technical difficulty is how mathematical guarantees can be provided about the result of such simulations. We seek to solve this difficulty by integrating ideas from many disciplines including optimization, optimal control, sensitivity analysis, robotic path planning techniques and statistical model checking to search for property violations and perform reach-while-avoid controller synthesis. Due to our focus on a simulation centered approach, the proposed approaches can be readily integrated into existing simulation environments that are commonly used in the industry such as Simulink/Stateflow(tm). The evaluation of our proposed approaches will be driven by the problem of verifying and synthesizing controllers for the Artificial Pancreas concept that promises to automate the delivery of insulin to diabetic patients using insulin pumps and continuous glucose monitors. Verifying these controllers will be essential to promote the public adoption of this technology, but also promises to be a moonshot for CPS verification. The plant models are nonlinear, hybrid systems and involve as many as 20 state variables. The controller itself is a model-predictive (MPC) controller that integrates an optimization engine as part of the controller. To our knowledge, the verification of reachability and safety properties for such a control system has not been attempted. Intellectual Merits: The use of simulations is essential in the presence of limited symbolic information about the system behavior. However, simulations present coverage issues that are hard to overcome, especially for systems with a large number of state variables. This proposal will formulate new ideas that can address the problems of using simulations in verification and synthesis procedures, while at the same time providing tangible guarantees about the result. To do so, we will explore a host of exciting ideas from optimization, optimal control theory, and statistical hypothesis testing to bear on this problem. Broader Impacts: The main broader impact of this proposal will be the availability of tools that can work inside commonly used model-based design and verification platforms such as Simulink/Stateflow(tm). One such tool resulting from an ongoing project (S-Taliro) is being actively used by engineers at Toyota to test automotive controller designs. The proposed work will build on the S-Taliro platform, yielding immediate benefits to many designers. We also propose a focus on the problem of verifying artificial pancreas (AP) controllers. Such a research will result in a fruitful engagement between our community and a community of engineers and physicians who are working hard to make the artificial pancreas concept a reality. Verification and synthesis techniques proposed here can help this effort immensely by identifying and fixing problems in the design before they can hurt patients and/or public confidence in this technology.
|Effective start/end date||10/1/13 → 9/30/17|
- NSF-CISE: Computer and Network Systems (CNS): $265,998.00