CAREER: Specializing Runtime Verification for Software Testing

软件测试通常是防止错误的最后一道防线。但是测试忽略了错误，因此昂贵且有害的错误经常出现在已部署的软件中。在测试过程中，需要能够帮助发现更多错误的技术。运行时验证就是这样一种技术；它通过检查程序运行是否符合描述正确程序行为的正式规范来发现bug。这个项目试图使运行时验证更加有效和高效。该项目还旨在通过创建关于运行时验证的课程，将运行时验证模块集成到软件测试课程中，以及创建公开可用的教学材料和开源工具，来促进对软件工程师的运行时验证教学。该项目着重于解决运行时验证使用的四个主要障碍：(1)大多数被标记的违反是假警报，因为现有的规范是不充分的；(2)确认一个违规信号是否为bug花费了太多的开发时间；(3)运行时验证不能扩展到社会日益依赖的大型软件系统；(4)对于开发人员来说，编写涵盖可能违反规范的代码的测试是昂贵的。解决这些障碍的自动化解决方案需要在运行时验证过程中生成的跟踪操作（程序事件序列）方面取得基本进展。因此，该项目将开发一种跟踪感知的运行时验证技术，该技术直接作用于跟踪。还将开发基于跟踪感知运行时验证的自动化技术，以实现以下目标：(1)通过修复现有规范来减少误报；(2)将每个违规行为归类为可能的bug或虚报；(3)减少运行验证过程中的冗余计算；(4)自动生成测试，以根据规范充分检查代码。该项目的主要影响是使运行时验证更接近于帮助开发人员在每次测试运行期间发现更多的错误。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Software testing is usually the last line of defense against bugs. But testing misses bugs, so costly and harmful bugs often occur in deployed software. Techniques that can help find more bugs during testing are needed. Runtime verification is one such technique; it finds bugs by checking program runs against formal specifications that describe correct program behavior. This project seeks to make runtime verification more effective and more efficient. The project also aims to facilitate teaching runtime verification to software engineers by creating a course on runtime verification, integrating runtime-verification modules into a software-testing course, and creating publicly available pedagogical materials and open-source tools.The project focuses on addressing four major impediments to runtime-verification usage: (1) most signaled violations are false alarms, because existing specifications are inadequate; (2) confirming whether a signaled violation is a bug takes too much developer time; (3) runtime verification does not scale to the large software systems on which society increasingly depends; and (4) it is expensive for developers to write tests that cover code where specifications may be violated. Automated solutions to address these impediments will require fundamental advances in operations on traces -- sequences of program events -- that are generated during runtime verification. Consequently, this project will develop a trace-aware runtime-verification technique that works directly on traces. Automated techniques based on trace-aware runtime verification will also be developed to (1) reduce false alarms by repairing existing specifications; (2) classify each violation as a likely bug or false alarm; (3) reduce redundant computations performed during runtime verification; and (4) generate tests automatically to adequately check code with respect to the specifications. The project's main impact is to bring runtime verification closer to helping developers find more bugs during every test run.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.