科研之友
微信
新浪微博
Facebook
分享链接
摘要
运行时验证是一种动态的软件验证技术，主要包括使用形式化规约描述待验证性质、自动生成对应监控器以及监控器的插桩.然而现有的面向C语言程序的运行时验证技术存在一些局限性，主要体现在多监控器的情况下，现有的运行时验证工具只能使用串行的方式处理，这大大降低了验证效率.因此，本文在分析了形式化规约的基础上，提出了一种基于无锁队列的运行时多线程并行验证方法.方法在现有工具MOVEC上实现并在测试集mibench上插桩运行，并与相关工具ACC、AC++和串行机制下的MOVEC进行了对比实验.实验结果表明，本文所实现的基于无锁队列的运行时多线程并行算法可以在有多个监控器的情况下有效地对C语言程序进行并行的运行时验证，且并行验证算法的性能比串行验证算法提升了约83%.
- 单位
