基于时间自动机的物联网服务建模和验证

被引：47

作者：

李力行 ^{[1
,2
]}

金芝 ^{[1
,3
]}

李戈 ^{[3
]}

机构：

[1] 中国科学院数学与系统科学研究院

[2] 中国科学院研究生院

[3] 高可信软件技术教育部重点实验室(北京大学)

来源：

计算机学报 | 2011年 / 34卷 / 08期

关键词：

物联网服务; 时间自动机; 环境实体; 服务建模; 模型验证;

D O I：

暂无

中图分类号：

TP301.1 [自动机理论]; TP391.44 []; TN929.5 [移动通信];

学科分类号：

摘要：

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

引用

页码：1365 / 1377

页数：13

共 4 条

[1] 需求驱动的Web服务建模及其验证:一个基于本体的方法
侯丽珊
金芝
吴步丹
[J]. 中国科学E辑:信息科学, 2006, (10) : 1189 - 1219
[2] Uppaal in a nutshell[J] . Kim G. Larsen,Paul Pettersson,Wang Yi.International Journal on Software Tools for Technology Transfer . 1997 (1-2)
[3] KRONOS: a verification tool for real-time systems[J] . Sergio Yovine.International Journal on Software Tools for Technology Transfer . 1997 (1-2)
[4] Automatic matchmaking of Web services. Agarwal S,Studer R. Proceedings of the IEEE International Conference on Web Services （ICWS’’06） . 2006

← 1 →