CAREER: Specializing Runtime Verification for Software Testing

职业：专门从事软件测试的运行时验证

• 批准号: 2045596
• 负责人: Owolabi Legunsen
• 金额: $ 58.59万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-06-01 至 2026-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2045596&HistoricalAwards=false
• 关键词: CAREER; Specializing; Runtime; Verification; Software

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.

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

项目成果

eMOP: A Maven Plugin for Evolution-Aware Runtime Verification

eMOP：用于 Evolution-Aware 运行时验证的 Maven 插件

• 发表时间: 2023
• 期刊: Springer
• 作者: Yorihiro, Ayaka;Jiang, Pengyue;Marques, Valeria;Carleton, Benjamin;Legunsen, Owolabi
• 通讯作者: Legunsen, Owolabi

Runtime Verification of Crypto APIs: An Empirical Study

• DOI: 10.1109/tse.2023.3301660
• 发表时间: 2023-10
• 期刊: IEEE Transactions on Software Engineering
• 影响因子: 7.4
• 作者: Adriano Torres;P. Costa;L. Amaral;Jonata T. Pastro;R. Bonifácio;Marcelo d’Amorim;Owolabi Legunsen;E. Bodden;Edna Dias Canedo

Extracting Inline Tests from Unit Tests

从单元测试中提取内联测试

• DOI: 10.1145/3597926.3598149
• 发表时间: 2023
• 期刊: ACM
• 作者: Liu, Yu;Nie, Pengyu;Guo, Anna;Gligoric, Milos;Legunsen, Owolabi
• 通讯作者: Legunsen, Owolabi

Comparing and combining analysis-based and learning-based regression test selection

比较和结合基于分析和基于学习的回归测试选择

• DOI: 10.1145/3524481.3527230
• 发表时间: 2022
• 期刊: IEEE/ACM International Conference on Automation of Software Test
• 作者: Zhang, Jiyang;Liu, Yu;Gligoric, Milos;Legunsen, Owolabi;Shi, August
• 通讯作者: Shi, August

Inline Tests

• DOI: 10.1145/3551349.3556952
• 发表时间: 2022-09
• 期刊: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering
• 作者: Yu Liu;Pengyu Nie;Owolabi Legunsen;Miloš Gligorić