FMitF: Track II: eMOP: A Tool for Evolution-Aware Runtime Verification

大多数软件开发人员执行回归测试，在每次代码更改后重新运行测试，以检查没有引入新的错误。不幸的是，回归测试经常遗漏bug。这个项目正在开发eMOP，这是一个运行时验证工具，用于在回归测试期间发现更多错误。运行时验证根据编码为逻辑公式的规范检查测试运行。不满足规范的测试运行将导致违规。该项目有三个基础设施重点。首先，创建一个核心eMOP组件，该组件增量地应用运行时验证，例如，通过仅重新检查受更改影响的代码部分中可能违反的规范。其次，核心组件与流行的开源回归测试基础设施集成：构建系统、持续集成和集成开发环境。第三，核心组件增强了优先级和改进的报告功能，使其更容易分类、检查和调试违规。完成后，eMOP将在开发人员已经使用的回归测试基础设施中提供运行时验证的bug查找好处。该项目将数十年运行时验证研究的成果带给了软件开发人员的广大受众。eMOP使开发人员能够更早地发现更多错误——理想情况下，在引入错误时立即发现错误。通过使用eMOP，学生还将在软件工程课程中了解轻量级的形式化方法。研究生和本科生，包括未被充分代表的少数民族，都将参与其中，他们将接触到软件工程和轻量级的形式化方法。eMOP代码将在Apache License 2.0下在GitHub （https://github.com/SoftEngResearch/emop）上公开发布。该守则将至少维持三年。从GitHub存储库链接的补充网页将包含教程和实验数据。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Most software developers perform regression testing, re-running tests after every code change, to check that new bugs are not being introduced. Unfortunately, regression testing often misses bugs. This project is developing eMOP, a runtime-verification tool for discovering more bugs during regression testing. Runtime verification checks test runs against specifications that are encoded as logical formulas. Test runs that do not satisfy the specifications result in violations.This project has three infrastructure thrusts. First, a core eMOP component is created that incrementally applies runtime verification, for example, by rechecking only specifications that can be violated in parts of code affected by the changes. Second, the core component is integrated with popular open-source regression testing infrastructure: build systems, continuous integration, and integrated development environments. Third, the core component is enhanced with features for prioritization and improved reporting that make it easier to triage, inspect, and debug violations. When complete, eMOP will offer the bug-finding benefits of runtime verification within regression testing infrastructure that developers already use.The project brings the results of decades of runtime verification research to a wider audience of software developers. eMOP enables developers to find more bugs earlier -- ideally as soon as the bugs are introduced. By using eMOP, students will also be introduced to lightweight formal methods within a software-engineering curriculum. Graduate and undergraduate students, including underrepresented minorities, will be involved, and they will gain exposure to software engineering and lightweight formal methods.The eMOP code will be released publicly on GitHub (https://github.com/SoftEngResearch/emop) under the Apache License 2.0. The code will be maintained for a minimum of three years. A supplementary web page linked from the GitHub repository will contain tutorials and experimental data.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.