| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | January 5, 2016 |
| Latest Amendment Date: | February 16, 2022 |
| Award Number: | 1552668 |
| Award Instrument: | Continuing Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | January 15, 2016 |
| End Date: | December 31, 2022 (Estimated) |
| Total Intended Award Amount: | $446,681.00 |
| Total Awarded Amount to Date: | $446,681.00 |
| Funds Obligated to Date: |
FY 2018 = $132,124.00 FY 2019 = $103,335.00 FY 2020 = $60,554.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
1601 VATTIER STREET MANHATTAN KS US 66506-2504 (785)532-6804 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
2 Fairchild Manhattan KS US 66506-1103 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Software & Hardware Foundation, CPS-Cyber-Physical Systems |
| Primary Program Source: |
01001819DB NSF RESEARCH & RELATED ACTIVIT 01001920DB NSF RESEARCH & RELATED ACTIVIT 01002021DB 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
Cyber-physical systems (CPSs) have become pervasive in the modern society, enabling transformative applications in the transportation, healthcare and energy sectors. However, the reliable development of CPSs remains an outstanding challenge. At the design level, hybrid systems theory provides a rich set of techniques and tools for ensuring correctness of high level functional properties such as safety and liveness. Current analysis techniques at the implementation level focus primarily on detecting low level runtime errors such as buffer overflows and divide by zero. A holistic approach to verifying functional specifications will considerably enhance the reliability scenario of CPSs development. This project investigates a robust verification methodology that guarantees functional correctness of the implementation by a "deeper" analysis on the design. More precisely, robust verification not only ensures that a design satisfies a given specification, but that small perturbations in the design still satisfy the specification. The perturbations on the design account for the deviations in the implementation with respect to the actual system. The proposed research investigates new foundations, abstractions and verification algorithms for robust analysis, in light of novel quantitative and/or topological aspects of robustness. In addition, prototype tools are developed to enable practical application and evaluation. The successful completion of the research will advance the knowledge in the fields of formal methods and hybrid control systems by leveraging ideas from control theory, dynamical systems theory, optimization theory and satisfiability modulo theory.
New cross-disciplinary courses at the undergraduate and graduate levels in hybrid control system design and analysis will be developed and taught. Activities for pre-college students involving programming with physical systems will be conducted towards increasing their interest in STEM related careers. Undergraduates, especially those from minority and underrepresented groups, will be recruited and mentored through involvement in research and outreach activities. The success of this research will force a quantum jump in the existing verification methodologies for CPSs, in particular, in the domains of automotive and aerospace systems, by bridging the gap in the analyses at the design and implementation phases.
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 developed algorithms and software tools for the robust analysis of cyber-physical systems (CPSs), that consist of software systems interacting with physical environments, to realize sophisticated objectives, as in driverless cars. The main focus of the project was to develop techniques for ensuring that CPSs behaved as expected even under uncertainties in the environment, thereby providing methodologies to build more reliable CPSs. The project considered the mathematical model of hybrid systems to capture the mixed discrete-continuous behaviors of CPSs that arise due to the interaction of discrete computer programs with continuous physical world. Stability, which captures a notion of robustness of the system behaviors to perturbations in the initial states and inputs, was considered. A novel algorithmic approach for stability analysis for hybrid systems was developed that consisted of reducing the stability analysis problem to structural problems on finite weighted graphs. First, a quantitative predicate abstraction technique that reduced Lyapunov and asymptotic stability analysis of linear hybrid systems to checking for absence of certain cycles in weighted graphs was developed. To address the coarseness in the abstraction method, a counter-example guided abstraction refinement technique was developed. This approach was extended to non-linear hybrid systems using the hybridization technique. These algorithms were further combined with region stability analysis to develop algorithms for global stability and were applied on automotive case studies. Further, robustness to uncertainties in the environment was considered and modeled by introducing stochasticity into the hybrid system model. Algorithms for safety and stability analysis of stochastic hybrid systems were developed based on abstraction-refinement techniques and applied to robot navigation case studies.
The results of this research have been published in over 15 papers that have appeared in major publication venues for computer science research. In addition, the software artifacts that have been developed in the course of this project are publicly available. The project has provided training opportunities for five graduate students who conducted research related to the project. One student has successfully graduated with a PhD during the project duration and has subsequently found employment as an assistant professor, while another student has graduated with a Masters degree. The remaining three students are currently in the second and/or third years of their PhD degrees, and made substantial progress. In addition, 5 undergraduate students were trained in topics related to cyber-physical systems, and 3 outreach events were conducted to teach robotic programming to K-12 students.
Last Modified: 05/25/2023
Modified by: Scott A Deloach
Please report errors in award information by writing to: awardsearch@nsf.gov.
