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

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

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.