| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 29, 2019 |
| Latest Amendment Date: | December 7, 2020 |
| Award Number: | 1918450 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Sandip Roy
CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | October 1, 2019 |
| End Date: | March 31, 2022 (Estimated) |
| Total Intended Award Amount: | $98,311.00 |
| Total Awarded Amount to Date: | $98,311.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
110 21ST AVE S NASHVILLE TN US 37203-2416 (615)322-2631 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
1025 16th Avenue S. Suite 102 Nashville TN US 37212-2328 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
FMitF: Formal Methods in the F, CPS-Cyber-Physical Systems |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
This project aims to transition recent research results that automate portions of the verification process of Cyber-Physical Systems into broader practice, particularly with industrial and student users. Cyber-physical systems (CPS) are networked embedded computing systems coupled with physics, such as in motor vehicles, aircraft, medical devices, and the electrical grid. Due to their frequent use in safety-critical scenarios where significant losses may be incurred, such as of human life or monetarily, the engineering process for such systems devotes vast resources to the process of verification to ensure these systems meet their requirements. The approach builds upon recent successes in the hybrid systems verification competition (ARCH-COMP) hosted in the past three years, in which several dozen hybrid systems verification tools have competed across several problem and system categories.
To achieve the transition of verification research results for CPS models into broader practice, this project develops a cloud-based framework to interface with and execute state-of-the-art formal verification software tools from the hybrid and dynamical systems verification community using NSF's CPS Virtual Organization (CPS-VO). The project extends the Design Studio and Tool Integration frameworks for the CPS-VO, to provide an easy-to-use interface for these verification tools. It also serves as a repository for housing executable versions of the tools and benchmarks, plus facilitating repeatability evaluations for ARCH-COMP through a distributed, cloud-based execution architecture. The core technology upon which the tool is built is the hybrid systems model source transformation and translation (HyST) software tool, which performs semantics-preserving translation between state-of-the-art hybrid systems verification tools.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
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 outcomes of this project are intellectual merit contributions through publications and other research products, broader impacts to the research community through competition and event organization, and the broader potential for future societal impact in domains dependent upon safety-critical cyber-physical systems (CPS), such as robotics. On intellectual merit, this project has helped lead to an understanding of what are the most effective verification approaches for CPS, enabled by the underlying hybrid systems source transformation and translation (HyST) technology. This technology has eased comparisons between state-of-the-art verification approaches in the hybrid systems domain by easing model interchange and comparison of results, helping to better illustrate which verification approaches may be most effective for different classes of systems, such as those with linear versus nonlinear dynamics. The project has also led to improvements in usability of these tools through the graphical interface to HyST and hybrid systems model checkers developed within WebGME.
For broader impacts, this project enabled the repeatability evaluation for the hybrid systems verification competition (ARCH-COMP), and the broader usage of the HyST technology by the community through the interactive design studio hosted on the CPS Virtual Organization (CPS-VO). These activities formed the basis of broader research community organizational activities, specifically the Artificial Intelligence and Neural Network Control Systems (AINNCS) category of ARCH-COMP, and the Verification of Neural Networks Competition (VNN-COMP), each of which have had broad participation by the relevant research communities. Altogether, the outcomes of the project may improve safety and reliability of systems in safety-critical domains.
Last Modified: 07/28/2022
Modified by: Taylor T Johnson
Please report errors in award information by writing to: awardsearch@nsf.gov.
