FMitF: Track II: FMCloak: Practitioners Using Formal Methods Without Knowing It

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.