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

工程团队通常会花大部分时间检查他们的设计是否正确运行，并在不正确时进行更改。 所有可能的使用都需要被预测并映射到不同的测试用例，这通常是不可行的，并且不可避免的错误和疏忽导致软件常见的永久补丁和更新周期。 这对于嵌入式和安全关键系统（如自动驾驶汽车）来说是不可接受的。 该项目自动生成监视器，作为添加到开发甚至部署的系统中的持续警惕的观察者。 故障由要检查的关键属性定义，例如不安全或未经批准的操作，监视器可以报告或可能减轻问题。 Unambient属性定义通常需要使用不熟悉的符号表示法，而该项目的新颖之处之一是使用伪英语。 该项目的影响包括使现有的工程人员能够补充传统的测试用例生成，并对组件或系统属性提供强有力的保证。监控生成被添加到跨国公司工程师使用的熟悉的开发环境中，他们评估对生产力和产品质量的影响。 虽然该工具最初需要在线性时序逻辑（LTL）中指定属性，但与NASA的合作将FRET工具纳入到将伪英语要求翻译为LTL中。 目前的增强功能包括生成具有不同性能、资源使用和隔离权衡的监视器，以适应开发和部署，为实时系统添加度量时间约束，以及自动合成监视器以确认状态转换的有效性和及时性。 统一的方法不需要针对软件、硬件和系统的不同工具，而是适合从硬件总线到完整的自动驾驶汽车的目标的运行时验证。 监控器的实现是以严格的数学方式自动分析正确性的，这减轻了工程师的责任。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.