| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 25, 2014 |
| Latest Amendment Date: | May 4, 2016 |
| Award Number: | 1422798 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Nina Amla
namla@nsf.gov (703)292-7991 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2014 |
| End Date: | August 31, 2018 (Estimated) |
| Total Intended Award Amount: | $500,000.00 |
| Total Awarded Amount to Date: | $515,000.00 |
| Funds Obligated to Date: |
FY 2016 = $15,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
506 S WRIGHT ST URBANA IL US 61801-3620 (217)333-2187 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
506 S Wright Street Urbana IL US 61801-3620 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
CSR-Computer Systems Research, Software & Hardware Foundation |
| Primary Program Source: |
01001617DB 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 widespread presence of embedded controllers in vehicles, medical devices, and water, power, and gas supply systems, makes the problem of ensuring their reliability critically important. The two most popular methods of achieving this in the context of cyberphysical systems, namely simulation and verification, suffer from serious drawbacks. Simulation, while being scalable and efficient, is incomplete. Verification, on the other hand, is computationally difficult and does not scale to large systems. This project explores a third approach where system-level correctness guarantees are derived from algorithmic analysis of finitely many, carefully chosen simulations or tests. The techniques developed in this project could enable more reliable and safe Cyber Physical Systems which are critically important class of systems.
This project will develop algorithms for finding the relationship between executions that start within close proximity of some initial state, techniques for verifying temporal properties involving non-linear propositions, and develop the foundations for compositional simulation-based verification. These ideas will be embodied in a software tool which will drastically reduce the effort required to verify cyberphysical models created using the Simulink/Stateflow environment. In addition to these research goals, the PIs plan on teaching a class on verifying hybrid systems that will introduce undergraduates and graduate students in engineering to the use of formal methods in embedded system design. The scientific ideas discovered, the tools built and the repository created will all be publicly disseminated.
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.
From self-driving cars to city-wide water, power, and gas supply systems, cyberphysical systems (CPS) have become pervasive. Reliability lapses of such CPS can cause major damage to infrastructure and people. In this project, we have developed new methods for finding design bugs in CPS. Previous methods were mostly applicable to linear system models whereas our approaches are applicable to more general nonlinear CPS, and thus, vastly extends the scope of this analysis. Our key technique relies on automatic sensitivity analysis of the system from models or data. Our techniques can not only help find bugs in existing system designs, but they can also help automatically synthesize controllers that meet requirements. This automation in synthesis can help save design engineers time and effort.
The main impacts of this project are the following: (a) We have created three open source software tools implementing the verification and synthesis algorithms: C2E2, DryVR, and RealSyn. These tools have advanced the state of the art, they have broken previous records in what was considered to be automatically verifiable or synthesizable, and they have been recognized by awards from the research community. For example, C2E2 was the first tool to automatically verify properties on an engine control system benchmark proposed as a challenge problem by researchers from Toyota. DryVR is the first tool to handle CPS that are described by a combination of blackbox simulators and formal models. Thus it is vastly more practical than previous tools. RealSyn can synthesize controllers for models with 20+ continuous dimensions advancing the state of the art in synthesis considerably. (b) Our approaches have advanced the understanding of how execution traces together with semantic analysis can be used in designing algorithms for verification and synthesis, with provable guarantees. This in turn has opened new research directions for the community, for example, related to sample complexity of these algorithms, possible parallelization, and other questions related to decidability and model equivalences. (c) The tools have been shown to be useful in a range of application domains from nonlinear and hybrid models of CMOS digital circuits, automotive driving assist systems like emergency braking, and power systems. We also show how this type of analysis can be used to assess the risk-level for automotive systems, which in turn plays a critical role in vehicle safety standards like ISO26262. Last but not least, the project has supported and sustained the research and educational activities of several students and faculty members including the creation of a new graduate level course at University of Illinois.
Last Modified: 01/14/2019
Modified by: Sayan Mitra
Please report errors in award information by writing to: awardsearch@nsf.gov.
