物联网服务的π-演算建模与验证

李文翔

(福建商学院 信息工程学院，福建 福州 350012)

物联网服务建模是物联网研究领域的一个分支，相比较于传统的服务，物联网服务具有实时性、资源约束性、位置相关性等性质。在物联网服务建模研究中，国内外学者做了大量的相关研究：李戈等[1]和李力行等[2]采用时间自动机理论建模物联网服务以及物理环境，并将用户期望的服务特性描述为时序逻辑公式，从而验证物联网服务运行于特定环境下能够满足期望的性质；针对基于自动机、Petri网等模型的状态空间爆炸问题，叶林等[3]提出使用微分动态逻辑和定量微分动态逻辑对物联网服务建模与验证；韩乔等[4]针对语义物联网服务的正确性验证问题，提出基于时态描述逻辑ALC-μ的语义物联网服务验证方法；马莉等[5]提出一种面向资源的物联网系统形式化建模与验证方法，使用通信顺序进程CSP对物联网系统的动态行为进行建模，利用线性时序逻辑LTL刻画待验证的性质；Yen等[6-7]扩展了现有OWL-S表达功能，将其用于对物联网服务的描述，并以此为基础讨论了物联网服务的组合问题；De等[8]基于本体语言分别对实体、资源和物联网服务进行语义建模；Sivrikaya等[9]针对智慧城市的具体应用，提出了一个服务识别和组合的分布式框架ISCO(intelligent framework for service discovery and composition)，在基于语义网的物联网服务和物理设备统一模型的基础上，使用OWL-S描述服务；为高效地获取物联网的各项资源(物理设备、物联网服务等)，Gomes等[10]提出了一个基于语义的资源识别服务QoDisco，该服务主要用于识别基于本体论进行语义描述的物联网各项资源。……