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

《程序验证的并行化方法研究与实现》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、濟料？雅衫園硕士学位论文Ｉ＾程序验证的并行化方法研究与实现作者姓名杨—豪＿指导教师姓名、职称段振华教授田聪教授＿工学硕申请学位翻＿±程序验证的并行化方法研究与实现作者姓名杨豪指导教师姓名、职称段振华教授田聪教授申请学位类别工学硕士学校代码10701学号1503121597分类号TP311密级公开西安电子科技大学硕士学位论文程序验证的并行化方法研究与实现作者姓名：杨豪一级学科：计算机科学与技术二级学科：计算机软件与理论学位类别：工学硕士指导教师姓名、职称：段振华教授田聪教授学院：计算机学院提交日

2、期：2018年6月TheresearchandimplementationofparallelizationmethodforprogramverificationAthesissubmittedtoXIDIANUNIVERSITYinpartialfulfillmentoftherequirementsforthedegreeofMasterinComputerSoftwareandTheoryByYangHaoSupervisor:DuanZhenhuaTitle:ProfessorSupervisor:Tian

3、CongTitle:ProfessorJune2018摘要摘要随着计算机技术的迅速发展，人类生活对计算机软件的依赖程度日益加深，在软件功能日益强大的同时，其复杂度和集成度也急剧增高，随之而来，软件漏洞所引发的灾难也频频发生，尤其在一些关键领域，一个软件漏洞就可能造成很严重的后果，因此，软件的安全性和可靠性急需得到保证。程序验证作为一种验证软件系统安全性和可靠性的验证技术，致力于确定一个系统是否正确完成了预设的目标。目前，程序验证已经广泛应用到软件安全相关的分析和验证中，并且取得了很大的成功。UMC4MSVL作为一个代

4、码级运行时验证工具，它使用建模仿真验证语言（ModelingSimulationandVerificationLanguage，MSVL）程序M描述系统，命题投影时序逻辑（PropositionalProjectionTemporalLogic，PPTL）公式P描述性质，动态执行包含系统和性质信息的程序来验证性质的有效性。该工具对程序中不同分支采用深度优先搜索的思想进行验证，验证完一条分支路径后，再去遍历验证其它分支路径。为了进一步提高程序验证的效率，本文基于多核计算机提供的硬件基础上，引入并行化的程序验证思想，实现

5、UMC4MSVL的并行化验证，同时验证多条分支路径，提高程序验证效率。本文的主要贡献分为以下几点：1.对UMC4MSVL验证器进行研究，包括验证原理、验证方法和工具实现，提出并行化验证的思想；2.设计UMC4MSVL的并行化验证框架并实现。实现多线程模块，将深度优先遍历的过程任务化并提交到任务队列，利用线程池技术同时执行多个任务进而同时验证多个分支路径；解决了并行验证过程中的变量互斥问题；实现了MSVL语句的并行化验证；并特别针对MSVL并行性语句的并行化验证提供了解决方案；3.实现反例路径输出功能，当性质不满足时，

6、可以输出导致性质不成立的执行路径，便于验证人员进行分析；4.通过幻方用例和狼羊菜用例测试了并行化验证的效率，通过一个简单用例和一个复杂用例测试了反例路径输出功能。关键词：MSVL，PPTL，UMC4MSVL，运行时验证，并行化IABSTRACTABSTRACTWiththerapiddevelopmentofcomputertechnology,humanlifehasbecomeincreasinglydependentoncomputersoftware.Assoftwarefunctionsbecomemore

7、powerful,itscomplexityandintegrationlevelhaveincreaseddramatically.Consequently,disasterscausedbysoftwarevulnerabilitieshavealsooccurredfrequently.Especially,insomekeyareas,asoftwarevulnerabilitymaycauseseriousconsequence.Therefore,thesecurityandreliabilityofso

8、ftwareneedtobeguaranteed.Programverification,asaverificationtechniqueforverifyingthesecurityandreliabilityofsoftwaresystems,isdedicatedtodeterminingwhetherasystemhascorrectl