| NSF Org: |
CNS Division Of Computer and Network Systems |
| Recipient: |
|
| Initial Amendment Date: | February 17, 2010 |
| Latest Amendment Date: | August 22, 2013 |
| Award Number: | 0953941 |
| Award Instrument: | Continuing Grant |
| Program Manager: |
Marilyn McClure
mmcclure@nsf.gov (703)292-5197 CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | March 1, 2010 |
| End Date: | February 29, 2016 (Estimated) |
| Total Intended Award Amount: | $459,648.00 |
| Total Awarded Amount to Date: | $459,648.00 |
| Funds Obligated to Date: |
FY 2011 = $89,558.00 FY 2012 = $91,332.00 FY 2013 = $187,890.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
3100 MARINE ST Boulder CO US 80309-0001 (303)492-6221 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
3100 MARINE ST Boulder CO US 80309-0001 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | CSR-Computer Systems Research |
| Primary Program Source: |
01001112DB NSF RESEARCH & RELATED ACTIVIT 01001213DB NSF RESEARCH & RELATED ACTIVIT 01001314DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
The goal of this project is to develop sophisticated formal verification tools for finding harmful defects in cyber-physical systems. Cyber-physical systems are responsible for numerous control tasks in safety-critical systems such as automobiles, avionics, medical devices, and power distribution systems. Guaranteeing the correctness of these systems is of the utmost importance. However, existing verification and validation techniques have fallen far short of addressing this important challenge.
This project investigates verification techniques for analyzing large and complex cyber-physical systems. First, the project is developing rich modeling formalisms that are capable of capturing realistic system designs at the right levels of abstraction. These formalisms form the basis for verification techniques that can be used to pinpoint functional defects in cyber-physical systems. Specifically, the project focuses on techniques for detecting harmful numerical precision loss in control systems implemented using fixed and floating point numbers. Finally, the project addresses the challenge of verifying complex non-linear systems using interval analysis, convex optimization and symbolic decision procedures. The results of this research are available to the community in the form of open-source tools. These tools will directly support the verification of complex systems.
The educational impact of the project lies in the integration of the research with a course curriculum centered around the theme of rigorous software engineering for cyber-physical systems. The resulting courses provide valuable training to undergraduate as well as graduate students in the use of advanced verification tools and techniques to ensure safe and reliable design of systems.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
The project sought to tackle three main challenges that made the verification of Cyber-Physical Systems (CPS) hard: (a) nonlinear models with large statespaces that defeated many verification approaches, (b) software systems with large number potentially infinitely many modes and (c) the absence of reliable tools usable by practitioners.
Work on this project has led to many significant directions for nonlinear CPS verification: (a) The tool Flow* was developed and has been significantly improved as part of this project. Flow* has been used to verify safety critical systems in automotive systems, medical devices and space systems by the CU Boulder team as well as CPS researchers from the industry. (b) We developed the concept of relational abstractions for handling continuous dynamics in the context of discrete system verification. Relationalization has enabled us to treat systems with software in the loop as part of the verification process. (c) Finally, we have developed ideas on solving nonlinear constraints efficiently to enable applications such as stability and invariance verification for closed loop systems.
The project involved 3 PhD students and 2 postdoctoral researchers, producing nearly 25 publications with two best paper awards. Furthermore, the project will significantly contribute to two PhD theses that will be submitted soon.
Broader Impacts
The work has led to numerous useful software systems for verifying nonlinear CPS designs. The Flow* tool has been especially useful for nonlinear flowpipe construction. It has been used by many researchers around the world to verify safety criticial systems.
As part of this project, the PI has developed courses on linear optimization. The successful on-campus deployment of this class led to a massively open online course that ran on Coursera. Nearly 40000 students enrolled and 2500 students around the world completed this course. The project has enabled the PI to offer courses on the verification of CPS at CU Boulder.
We expect to continue development of these ideas to handle larger and more realistic CPS designs. In doing so, we hope to make future CPS designs safer while at the same time keeping the development costs under control through the automation of verification. Ultimately, this will benefit the society at large in the form of highly reliable medical devices and autonomous vehicles.
Last Modified: 06/15/2016
Modified by: Sriram Sankaranarayanan
Please report errors in award information by writing to: awardsearch@nsf.gov.
