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

• 作者: 李力行 李戈 金芝
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 物联网服务 时间自动机 环境实体 服务建模 模型验证
• 年，卷（期）: 2011,（8）
• 所属期刊栏目: 物联网关键理论与技术
• 页码范围: 1365-1377
• 分类号: TP393
• 字数: 12323字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2011.01365

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李力行	中国科学院数学与系统科学研究院	4	111	4.0	4.0