基于aspcsp并发系统模型验证的研究

《基于aspcsp并发系统模型验证的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、独创性（或创新性）声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中不包含其他人已经发表或撰写过的研究成果；也不包含为获得桂林电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处，本人承担一切相关责任。本人签名：日期：关于论文使用授权的说明本人完全了解桂林电子科技大学有关保留和使用学位论文的规定，即：研究生在校攻读学位期间论文工作的知识产权单位属桂林电子科技大学。本人保证毕业

2、离校后，发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有权保留送交论文的复印件，允许查阅和借阅论文；学校可以公布论文的全部或部分内容，可以允许采用影印、缩印或其它复制手段保存论文。（保密的论文在解密后遵守此规定）本学位论文属于保密在____年解密后适用本授权书。本人签名：日期：导师签名：日期：摘要摘要并发系统是现实世界中一类重要的复杂系统，已广泛应用于军事、交通、商业和服务业中，纵观现代软件行业，从操作系统到互联网，并发程序无处不在。虽然并发程序在当前有着广泛的应用，但程序的并发特性也使得程序语义具有不确定性，从而使并发程序性质的验证研究较顺序程序要困难

3、得多。模型检测是主流的并发系统验证技术。但多数并发系统模型验证工具不支持在系统的一次运行中验证多个性质，从而也降低了性质验证的效率。该问题在现有的主流模型检测框架内很难克服。通信顺序进程(Communicationsequentialprocess,简称：CSP)是一种具有严格数学理论支持的描述并发进程之间相互作用模式的进程代数语言，已经在网络协议建模、并发系统验证以及计算机软硬件设计方面得到广泛的应用。本文研究以CSP语言描述的并发系统性质的验证问题，构建基于回答集编程(AnswerSetProgramming,简称：ASP)的CSP并发系统验证框架，解决上述讨论的并发

4、系统验证方法中的问题。具体地，本文主要研究成果如下：(1)提出了将CSP模型转换为ASP程序的方法，讨论了CSP进程的顺序、循环和选择结构的ASP程序描述，给出了CSP的并发执行规则的ASP描述。研究了把待验证系统性质转化为ASP规则的技术，给出了LTL、CTL公式到ASP规则的转换方法。(2)在此基础上开发了基于ASP的CSP并发系统验证原型系统。实验结果表明该技术易于实现，在保持较高验证效率的同时，能够支持在验证软件的一次执行中验证多条LTL/CTL公式。(3)提出了CSP并发系统性质不满足时生成反例的技术，把ASP程序支撑原因分析技术应用于CSP模型验证性质反例生成

5、研究，给出了相应的反例生成算法，实例表明了该技术的有效性。关键词：回答集编程；通信顺序编程；程序并发；LTL/CTL公式；ASP程序调试；-I-AbstractAbstractAsakindofimportantandcomplexsystems,concurrentsystemshavebeenwidelyusedinmilitary,transportation,commercialandserviceindustry.Concurrentprogramsareubiquitousinthemodernsoftwareindustryfromoperationsyst

6、emstotheinternet.Concurrencycausedbytheuncertaintyofprogramsemantic,however,alsomakesthepropertycheckingofconcurrentprogramsharderthanthatofsequentialprograms.Modelcheckingisamainstreamtechnologyfortheverificationofconcurrentsystems.Unfortunately,mostmodelcheckersdonotsupporttheverificati

7、onofmultiplepropertiesinonerunoftheverifiers,leadingtoareductioninthepropertycheckingefficiency.Thisproblemishardtosolveintheexistingpopularmodelcheckingframework.Communicationsequentialprocess(CSP)isaprocessalgebralanguagewithstrictmathematicaltheorysupportandisuse