基于模态逻辑的模型检测技术研究

《基于模态逻辑的模型检测技术研究》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、分类号：密级：编号：UDC：工学博士学位论文基于模态逻辑的模型检测技术研究博士研究生：陈志远指导教师：黄少滨教授学科、专业：计算机应用技术哈尔滨工程大学2014年3月 分类号：密级：编号：UDC：工学博士学位论文基于模态逻辑的模型检测技术研究博士研究生：陈志远指导教师：黄少滨教授学位级别：工学博士学科、专业：计算机应用技术所在单位：计算机科学与技术学院论文提交日期：2013年12月论文答辩日期：2014年03月学位授予单位：哈尔滨工程大学 ClassifiedIndex:U.D.C:ADissertationfortheDe

2、greeofD.EngResearchofModelCheckingTechniquebasedonModalLogicCandidate:ChenZhiyuanSupervisor:Prof.HuangShaobinAcademicDegreeAppliedfor:DoctorofEngineeringSpecialty:ComputerAppliedTechnologyDateofSubmission:December,2013DateofOralExamination:March,2014University:Harbin

3、EngineeringUniversity 哈尔滨工程大学学位论文原创性声明本人郑重声明：本论文的所有工作，是在导师的指导下，由作者本人独立完成的。有关观点、方法、数据和文献的引用已在文中指出，并与参考文献相对应。除文中已注明引用的内容外，本论文不包含任何其他个人或集体已经公开发表的作品成果。对本文的研究做出重要贡献的个人和集体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。作者（签字）：日期：年月日哈尔滨工程大学学位论文授权使用声明本人完全了解学校保护知识产权的有关规定，即研究生在校攻读学位期间论文工作

4、的知识产权属于哈尔滨工程大学。哈尔滨工程大学有权保留并向国家有关部门或机构送交论文的复印件。本人允许哈尔滨工程大学将论文的部分或全部内容编入有关数据库进行检索，可采用影印、缩印或扫描等复制手段保存和汇编本学位论文，可以公布论文的全部内容。同时本人保证毕业后结合学位论文研究课题再撰写的论文一律注明作者第一署名单位为哈尔滨工程大学。涉密学位论文待解密后适用本声明。本论文（□在授予学位后即可□在授予学位12个月后□解密后）由哈尔滨工程大学送交有关部门进行保存、汇编等。作者（签字）：导师（签字）：日期：年月日年月日 基于模态逻辑的模型

5、检测技术研究摘要模态逻辑是逻辑学领域最重要的分支之一。特别是克里普克可能世界语义学的建立，使模态逻辑有了准确可靠的语义模型，促进了模态逻辑的快速发展。模型检测技术是形式化验证领域的重要组成部分，可以对软硬件系统的正确性进行高度自动化的验证，在软件工程领域和工业界备受瞩目。而如何避免状态空间爆炸问题、系统性质正确描述和长反例理解是模型检测技术面临的三个主要挑战。如何将模态逻辑这一强大工具有效地应用到模型检测技术中，提高对大型复杂系统进行检测的能力，从而保证系统的可靠性与安全性是一项意义重大的工作，同时也是理论计算机科学与软件工程领

6、域的一个重要研究内容。针对该课题，本文主要在以下几个方面进行了研究：（1）提出了一种有限状态迁移系统模型的状态空间约简方法。该方法通过适当选取自函子的终结余代数，通过模态逻辑理论中的互模拟等价关系来产生最小的有限状态迁移系统模型。使得该迁移系统能够完全等价地模拟原迁移系统的所有行为，保证系统验证的等效性，有效地避免对系统进行模型检测时的状态空间爆炸问题。（2）在Global作用域下构造了一类可以正确描述系统性质的抽象CTL公式模板。首先，通过对系统性质与系统行为进行研究，阐述了以组合命题作为模式与作用域参数的形式化描述研究的可行

7、性与必要性。然后，通过对线性时序逻辑LTL与分支时序逻辑CTL的研究，给出了用CTL描述系统性质的方法。同时，通过重新定义的三个逻辑运算符来简化公式，使构造的CTL公式模板更加简洁，易于理解。最后，构造出Global作用域下所有模式的CTL公式模板，用来生成由组合命题类、模式和作用域定义的描述系统复杂性质和行为的CTL公式。针对所构造的CTL公式模板，给出了模板正确性的证明，说明该方法构造的CTL公式模板可以生成正确的CTL公式。（3）在Before等作用域下构造了可以正确描述系统性质的抽象CTL公式模板，从而完善了所有作用域与

8、模式组合的CTL公式模板类。首先，通过对将来区间逻辑FIL的语法和语义研究，说明将来区间逻辑FIL在刻画系统性质和系统行为方面表达能力的不足。特别是对Prospec描述结果的表示形式上，CTL无疑具有不可替代的优势，而且CTL也是现在众多优秀模型检测器的输入语言