基于图论的形式化验证方法的研究与实现

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

1、朵各糾成＊穿ＵＮＩＴＹＦＥＬＥＣＴＲＩＥＮＣＥＡＮＤＴＥ已ＨＮＯＬＯＧＹＯＦＣＨＩＮＡＩＶＥＲＳＯＯＮＩＣＳＣ专业学位硕±学位论文ＭＡＳＴＥＲＴＨＥＳＩＳＦＯＲＰＲＯＦＥＳＳＩＯＮＡＬＤＥＧＲＥＥｒ画ｉ论支题目基于图论的形式化验证方法的妍究与实现专业学位类别工程硕±学号２０１３２２２２０２２８作者娃名陈凌字指导教师詹谨瑜副繼■定独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。据我所知，除了文中特别加标注和致谢的地

2、方外，论文中不包含其他人己经发表或撰写过的研究成果，也不包含为获得电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。作者签名：常足寺曰期；巧／＾年＾月／２曰论文使用授权本学位论文作者完全了解电子科技大学有关保留、使用学位论文的规定，有权保留并向国家有关部口或机构送交论文的复印件和磁盘，化许论文被查阅和借瞬。本人授权电子科技大学可臥将学位论文、的全部或部分内容编入有关数据库进行检索，可Ｗ采用影印缩印或扫描等复制手段保存、汇

3、编学位论文。）（保密的学位论文在解密后应遵守此规定作者签名：带导师签名：诲＞＾＾＾日期：年（月攻日，分类号密级注1UDC学位论文基于图论的形式化验证方法的研究与实现陈凌宇指导教师詹瑾瑜副教授电子科技大学成都申请学位级别硕士专业学位类别工程硕士工程领域名称软件工程提交论文日期2016.03.18论文答辩日期2016.04.27学位授予单位和日期电子科技大学2016年6月答辩委员会主席评阅人RESEARCHANDIMPLEMENTATIONOFMODELCHECKINGALGORITHMBASEDONGRAHPTHEORYAM

4、asterThesisSubmittedtoUniversityofElectronicScienceandTechnologyofChinaMajor:MasterofEngineeringAuthor:ChenLingyuSupervisor:ZhanJinyuSchoolofInformationandSoftwareSchool:Engineering摘要摘要随着硬件制作的工艺发展和软件开发技术的日益成熟，软硬件的制作产能越来越强，这也对软硬件质量的可靠性和效率性能有了越来越高的要求。为此在可靠性和性能的保证上的资源投入也越来越大。传

5、统验证方法会耗费太多的人力物力。为了降低制作和开发的成本，同时保证其产品的可靠性，基于严格的数据证明的验证方法形式化验证，也越来越受到人们的重视，在工业界有了广泛的使用。在科学界，形式化验证的方法也有了很多分支和广泛了研究。本文深入研究了现有的形式化验证方法，提出了一种新的形式化验证方法。该方法采用图的邻接矩阵建立待验证系统的数学模型，采用CTL表示式来描述待验证系统需要满足的属性，将待验证系统的属性验证过程转化成了对应矩阵模型的计算。本文首先给出了一种基于邻接矩阵的系统建模方法，根据待验证系统状态图中的各状态编码和状态转移关系，给出待验证系

6、统状态图的邻接矩阵，由于该矩阵与待验证系统同构，因此可以通过邻接矩阵的相关运算来反映待验证系统的各个属性。本验证方法改进了模型检测算法中复杂的状态标记过程，为不同时态逻辑CTL运算符分别给出了对应的矩阵运算表示，使得待验证系统的形式化验证过程变成了矩阵的公式计算，根据需验证的CTL属性描述带入相应的矩阵计算公式即可方便地计算出其可满足性。本文最后采用所提出的基于图邻接矩阵的形式化验证方法，设计并实现了一个形式化验证工具，并通过对两个实例（FIFO队列和PCI总线仲裁器）的验证以及与NuSMV工具的验证结果对比，说明了本文方法及其工具的可用性和

7、有效性。关键词：形式化验证，模型检测，Kripke结构，CTL表达式，邻接矩阵IABSTRACTABSTRACTWiththedevelopmentofhardwareproductivityandsoftwaretechnology,thereliabilityandefficiencyofhardwareandsoftwarebecomemoreandmoreimportant.Thehigherrequirementcausemorecost.Thetraditionalverificationmethodsneedtoomuchman

8、powerandmaterialresources.Inordertoreducethecostofproductionanddevelopmentandensur