文献类型：期刊文章

作　　者：李力行[1,2] 金芝[1,3] 李戈[3]

机构地区：[1]中国科学院数学与系统科学研究院,北京100190 [2]中国科学院研究生院,北京100049 [3]高可信软件技术教育部重点实验室(北京大学),北京100871

出　　处：《计算机学报》

基　　金：国家"九七三"重点基础研究发展规划项目基金(2011CB302704);国家自然科学基金青年科学基金项目(60803010)资助~~

年　　份：2011

卷　　号：34

期　　号：8

起止页码：1365-1377

语　　种：中文

收录情况：BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20113714332521)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：物联网服务的建模和验证是当前物联网服务提供中的一个重要问题.文中将物联网服务的行为建模为其与相关环境实体的交互,并引入环境实体以刻画物理世界各种物体的属性和行为,从而将物联网服务能力建模为它能够导致的环境实体发生的期望变化.文中以时间自动机为建模工具,分别为将要监测和要控制的物理环境实体以及不同种类的物联网服务独立建模,以表现它们的独立性和自主性.这些时间自动机形成一个网络,刻画完整的物联网服务的通信并发过程,物联网服务的实施过程表现为时间自动机网络上的状态变迁通路.最后,文中提出一组物联网服务要满足的性质,并利用模型检测工具UPPAAL验证物联网服务的正确性.

关 键 词：物联网服务  时间自动机 环境实体 服务建模  模型验证  

分 类 号：TP393]