论文部分内容阅读
随着计算机技术的迅速发展,人类生活对计算机软件的依赖程度日益加深,在软件功能日益强大的同时,其复杂度和集成度也急剧增高,随之而来,软件漏洞所引发的灾难也频频发生,尤其在一些关键领域,一个软件漏洞就可能造成很严重的后果,因此,软件的安全性和可靠性急需得到保证。程序验证作为一种验证软件系统安全性和可靠性的验证技术,致力于确定一个系统是否正确完成了预设的目标。目前,程序验证已经广泛应用到软件安全相关的分析和验证中,并且取得了很大的成功。UMC4MSVL作为一个代码级运行时验证工具,它使用建模仿真验证语言(Modeling Simulation and Verification Language,MSVL)程序M描述系统,命题投影时序逻辑(Propositional Projection Temporal Logic,PPTL)公式P描述性质,动态执行包含系统和性质信息的程序来验证性质的有效性。该工具对程序中不同分支采用深度优先搜索的思想进行验证,验证完一条分支路径后,再去遍历验证其它分支路径。为了进一步提高程序验证的效率,本文基于多核计算机提供的硬件基础上,引入并行化的程序验证思想,实现UMC4MSVL的并行化验证,同时验证多条分支路径,提高程序验证效率。本文的主要贡献分为以下几点:1.对UMC4MSVL验证器进行研究,包括验证原理、验证方法和工具实现,提出并行化验证的思想;2.设计UMC4MSVL的并行化验证框架并实现。实现多线程模块,将深度优先遍历的过程任务化并提交到任务队列,利用线程池技术同时执行多个任务进而同时验证多个分支路径;解决了并行验证过程中的变量互斥问题;实现了MSVL语句的并行化验证;并特别针对MSVL并行性语句的并行化验证提供了解决方案;3.实现反例路径输出功能,当性质不满足时,可以输出导致性质不成立的执行路径,便于验证人员进行分析;4.通过幻方用例和狼羊菜用例测试了并行化验证的效率,通过一个简单用例和一个复杂用例测试了反例路径输出功能。