基于时态描述逻辑的语义物联网服务验证

摘要

随着信息时代的来临，物联网早已成为信息化发展中不可或缺的一部分。为了使物联网更加智能化，将语义引入物联网中，形成语义物联网。将语义物联网与面向服务的方法相结合，可以高效的利用物联网中的信息资源。而语义物联网服务的正确与否却是一个有待验证的问题。
　　针对语义物联网服务的正确性验证问题，文中采用描述逻辑与传统时态逻辑相结合的方式。使用描述逻辑对系统建模中的领域知识进行刻画，同时引入领域知识推理机制，将其与传统的模型检测机制相融合。
　　本文首先在领域知识的驱动下，利用带有ABox标注的状态迁移系统对语义物联网服务进行建模，其次将描述逻辑ALC分别与命题μ-演算和概率计算树逻辑相结合对待验证性质进行刻画，并给出具体的模型检测算法。
　　研究工作如下：
　　（1）给出了一种基于时态描述逻辑 ALC-μ的建模和验证方法。时态描述逻辑ALC-μ是将描述逻辑的刻画能力与命题μ-演算的表示能力相结合后的一种逻辑系统。在命题μ-演算的基础上构建了时态描述逻辑ALC-μ，一方面使用μ-演算的时态算子表示系统的性质，另一方面使用描述逻辑对领域知识进行刻画。并针对上述所构建的逻辑系统，提出时态描述逻辑ALC-μ的模型检测算法。与命题μ-演算相比较，该模型检测算法将描述逻辑ALC的推理机制与模型检测机制相融合，可以用来对语义物联网服务的正确性进行验证。并且为了更好的将理论应用于实际，在 ALC-μ的模型检测算法的基础上开发出相应的验证软件。
　　（2）给出了一种基于概率时态描述逻辑ALC-PCTL的建模和验证方法。首先，利用描述逻辑中的ABox对概率自动机进行标注，引入语义标注的概率有限自动机对语义物联网服务进行建模。其次，将描述逻辑ALC与概率计算树逻辑相结合，构建概率时态描述逻辑ALC-PCTL，用其对待验证的时态性质进行刻画。最后，给出将概率模型检测机制与描述逻辑推理机制相结合的模型检测算法，用来对语义物联网服务的正确性进行验证。

目录

声明

第一章 绪 论

§1.1 研究背景及意义

§1.2 国内外研究现状

§1.3 研究内容

§1.4 文章结构

第二章 相关基础知识介绍

§2.1 命题μ-演算

§2.2 描述逻辑ALC

§2.3 概率分支时态逻辑PCTL

§2.4 语义物联网服务架构

§2.5 本章总结

第三章 时态描述逻辑ALC-μ

§3.1 引言

§3.2 基于时态描述逻辑ALC-μ的系统建模

§3.3 时态描述逻辑ALC-μ

§3.4 基于时态描述逻辑ALC-μ的模型检测算法

§3.5 小结

第四章 概率时态描述逻辑ALC-PCTL

§4.1 引言

§4.2 基于ALC-PCTL的系统建模

§4.3 概率时态描述逻辑ALC-PCTL

§4.4 ALC-PCTL的模型检测算法

§4.5 小结

第五章 ALC-μ验证工具

§5.1 引言

§5.2 系统设计与实现

§5.3 工具演示

§5.4 本章小结

第六章 结束语

§6.1 主要研究工作总结

§6.2 研究展望

参考文献

致谢

攻读硕士学位期间发表或录用的论文