程序验证的并行化方法研究与实现

发布时间：2021-03-17 21:50

　　随着计算机技术的迅速发展,人类生活对计算机软件的依赖程度日益加深,在软件功能日益强大的同时,其复杂度和集成度也急剧增高,随之而来,软件漏洞所引发的灾难也频频发生,尤其在一些关键领域,一个软件漏洞就可能造成很严重的后果,因此,软件的安全性和可靠性急需得到保证。程序验证作为一种验证软件系统安全性和可靠性的验证技术,致力于确定一个系统是否正确完成了预设的目标。目前,程序验证已经广泛应用到软件安全相关的分析和验证中,并且取得了很大的成功。UMC4MSVL作为一个代码级运行时验证工具,它使用建模仿真验证语言（Modeling Simulation and Verification Language,MSVL）程序M描述系统,命题投影时序逻辑（Propositional Projection Temporal Logic,PPTL）公式P描述性质,动态执行包含系统和性质信息的程序来验证性质的有效性。该工具对程序中不同分支采用深度优先搜索的思想进行验证,验证完一条分支路径后,再去遍历验证其它分支路径。为了进一步提高程序验证的效率,本文基于多核计算机提供的硬件基础上,引入并行化的程序验证思想,实现UM... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：88 页

【学位级别】：硕士

【部分图文】：

验证操作示例

验证进程信息

(a)(b)图5.3 狼羊菜用例测试对比图 5.3 中图 5.3(a)是串行的 UMC4MSVL 验证器的验证结果，图 5.3(b)是线程池大小设为 4 下的并行化验证结果。

【参考文献】：
期刊论文
[1]二维逻辑PPTLSL的可满足性检查[J]. 陆旭,段振华,田聪.  软件学报. 2016(03)
[2]一个命题投影时序逻辑符号模型检测器[J]. 逄涛,段振华,刘晓芳.  软件学报. 2015(08)
[3]构造偶阶幻方的一个算法[J]. 段振华.  微电子学与计算机. 1990(04)

博士论文
[1]面向对象MSVL语言及其在组合Web服务验证中的应用[D]. 王小兵.西安电子科技大学 2009



本文编号：3087769