《计算机学报》文章摘要   全文下载
文章题目	基于时间自动机的物联网服务建模和验证
作者	李力行1),2) 金芝1),3) 李戈3)
作者单位	1)(中国科学院数学与系统科学研究院 北京 100190) 2)(中国科学院研究生院 北京 100049) 3)(高可信软件技术教育部重点实验室(北京大学) 北京 100871)
发表年份	2011
发表月份	8期(1365—1377)
文章摘要	摘要 物联网服务的建模和验证是当前物联网服务提供中的一个重要问题.文中将物联网服务的行为建模为其与相关环境实体的交互，并引入环境实体以刻画物理世界各种物体的属性和行为，从而将物联网服务能力建模为它能够导致的环境实体发生的期望变化.文中以时间自动机为建模工具，分别为将要监测和要控制的物理环境实体以及不同种类的物联网服务独立建模，以表现它们的独立性和自主性.这些时间自动机形成一个网络，刻画完整的物联网服务的通信并发过程，物联网服务的实施过程表现为时间自动机网络上的状态变迁通路.最后，文中提出一组物联网服务要满足的性质，并利用模型检测工具UPPAAL验证物联网服务的正确性. 关键词 物联网服务；时间自动机；环境实体；服务建模；模型验证 中图法分类号 TP393 DOI号: 10.3724/SP.J.1016.2011.01365