Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Doing Business As Name:Virginia Polytechnic Institute and State University
  • Cameron D Patterson
  • (540) 231-8397
Award Date:06/08/2021
Estimated Total Award Amount: $ 99,999
Funds Obligated to Date: $ 99,999
  • FY 2021=$99,999
Start Date:10/01/2021
End Date:03/31/2023
Transaction Type:Grant
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:FMitF: Track II: FMCloak: Practitioners Using Formal Methods Without Knowing It
Federal Award ID Number:2123550
DUNS ID:003137015
Parent DUNS ID:003137015
Program:FMitF: Formal Methods in the F
Program Officer:
  • Anindya Banerjee
  • (703) 292-7885

Awardee Location

Street:Sponsored Programs 0170
Awardee Cong. District:09

Primary Place of Performance

Organization Name:Virginia Polytechnic Institute and State University
Street:1145 Perry St
Cong. District:09

Abstract at Time of Award

Engineering teams typically spend most of their time checking whether their designs function correctly and making changes when they do not. All possible usages need to be anticipated and mapped to distinct test cases, which is generally infeasible, and the inevitable bugs and oversights result in perpetual patch and update cycles common for software. This is less acceptable for embedded and safety critical systems such as autonomous vehicles. The project automatically generates monitors serving as continuously vigilant observers added to the development or even the deployed system. Monitors are defined by the critical properties to be checked, such as unsafe or unsanctioned actions, and a monitor may report or possibly mitigate the problem. Unambiguous property definitions normally require use of an unfamiliar symbolic notation, and one of the project’s novelties is to instead use pseudo-English. The project’s impacts include enabling the existing engineering workforce to supplement conventional test case generation with strong assurances about component or system properties. Monitor generation is being added to familiar development environments used by a multinational corporation’s engineers, who evaluate the effect on productivity and product quality. While the tool originally required properties to be specified in linear temporal logic (LTL), a collaboration with NASA incorporated the FRET tool to translate pseudo-English requirements to LTL. Current enhancements include the generation of monitors with different performance, resource usage and isolation tradeoffs to suit both development and deployment, adding metric time constraints for real-time systems, and automatically synthesizing monitors to confirm state transition validity and timeliness. Rather than require distinct tools for software, hardware and systems, a unified approach suits run-time verification of targets ranging from hardware buses to complete autonomous vehicles. Monitor implementations are automatically analyzed for correctness in a mathematically rigorous way, which relieves engineers of that responsibility. 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.

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.