时态描述逻辑DL-CTL的模型检测技术研究

摘要

模型检测是一种广泛应用的形式化验证技术，它不仅有高效的验证算法作为理论基础，而且成熟的验证工具使其在工业界得到了广泛的应用。描述逻辑（DL）是一种随着语义Web的发展而受到广泛关注的逻辑系统。它虽然具有表达能力强且可判定的优点，但只能刻画静态领域的知识。因此，研究者分别从时态和动态领域对描述逻辑进行扩展，分别得到时态描述逻辑（TDL）和动态描述逻辑（DDL）。　　本文主要将描述逻辑的这些扩展引入到模型检测技术中。目前，在该领域已经有研究成果中，它们验证的性质大都是线性的，虽然也出现了对分支性质验证的尝试，但并没有利用描述逻辑丰富的推理机制；与此同时，在将动作理论引入到模型检测技术中的时候，仅考虑了原子动作，并没有考虑诸如“选择”、“迭代”等动态描述逻辑DDL中的复杂动作。　　本文利用分支时态描述逻辑DL-CTL和动态描述逻辑DDL，结合模型检测技术，来解决上述的问题，主要的研究内容如下：　　1.研究时态描述逻辑DL-CTL的模型检测问题。一方面，在模型建立时，基于描述逻辑DL的知识库对背景知识和模型中状态的性质进行描述；另一方面，采用时态描述逻辑 DL-CTL公式对待验证的性质进行刻画。最后，形式化地定义时态描述逻辑DL-CTL模型检测问题的，并结合描述逻辑相关的推理机制，研究得到其模型检测算法。　　2.设计并开发时态描述逻辑DL-CTL的模型检测工具。以研究得到的时态描述逻辑DL-CTL模型验证算法为基础，设计并开发了基于DL-CTL的模型验证工具。该工具能够完成知识库的建立、系统模型的创建、时态公式输入、验证等核心功能。利用这些功能，该工具能够快速方便地验证时态逻辑公式在系统模型中是否成立。　　3.研究引入动作理论的DL-CTL的模型检测问题。一方面，在传统的模型检测技术基础上，将动态描述逻辑DDL中原子动作的执行作为系统模型中状态间的迁移原因；另一方面，采用时态描述逻辑DL-CTL公式描述待验证的时态规范。在此基础上，形式化定义了引入动作理论之后的模型检测问题。借助描述逻辑成熟的推理机制，本文提出与之相应的验证算法，并通过具体的实例来验证该方法的可行性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

§1.1 研究背景及意义

§1.2 研究现状

§1.3 研究内容

§1.4 文章结构

第二章 相关基础知识

§2.1 分支时态逻辑CTL

§2.2 时态描述逻辑DL-CTL

§2.3 基于描述逻辑的动作理论

§2.4 小 结

第三章 时态描述逻辑DL-CTL的模型检测

§3.1 引 言

§3.2 预备知识

§3.3 DL-CTL的模型检测算法

§3.4 实例分析

§3.6 小 结

第四章 DL-CTL模型检测工具的设计和实现

§4.1 引 言

§4.2 系统整体设计

§4.3 系统演示

§4.4 小 结

第五章 引入动作理论的时态描述逻辑DL-CTL的模型检测

§5.1 引 言

§5.2 预备知识

§5.3 引入动作理论的DL-CTL模型检测算法

§5.4 实例说明

§5.5 小 结

第六章 总结与展望

§6.1 研究工作总结

§6.2 研究前景展望

参考文献

致谢

攻读硕士学位期间研究成果