一种基于路径切片的并行运行时验证方法
李佳洁
陈哲
南京航空航天大学计算机科学与技术学院 南京 211106
摘要：运行时验证是一种在程序运行过程中对程序行为进行正确性验证的技术,已被应用到诸多领域.运行时验证中使用监控器规约描述性质,监控器规约中可以定义多个性质.然而,现有运行时验证技术存在性能方面的缺陷:当监控器规约中定义了多个性质时,现有技术只能采用串行的方式对多个性质进行验证,导致程序的运行时性能很差,从而限制了运行时验证的实用性.因此为了提高运行时验证的效率,提出了一种基于路径切片的并行运行时验证方法,并对现有工具MOVEC进行功能扩展,实现了上述并行运行时验证方法.不仅如此,还在测试集Mibench上与串行机制下的MOVEC进行了对比实验.实验结果表明,基于路径切片的并行运行时验证方法可以实现对C语言程序的有效并行验证,且性能可以提高约70%,达到了更多地利用计算资源,更快地验证程序正确性的目的.
关键词：运行时验证监控器规约并行路径切片哈希层次森林
分类号：TP301.2(计算技术、计算机技术)
资助基金：国家自然科学基金(62172217)国家自然科学基金(U533130)中央高校基本科研业务费人工智能+专项(NZ2020019)
论文发表日期：2025-12-20
在线出版日期：2026-03-09（本平台首次上网日期，不代表文献的发表时间）
页数：7( 3470-3476 )
英文信息