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

CORC > 北京大学

	基于时间自动机的物联网服务建模和验证
	李力行 ; 金芝 ; 李戈
刊名	http://epub.edu.cnki.net/grid2008/brief/detailj.aspx?filename=JSJX201108004&dbname=CJFQ2011
	2012-04-25 ; 2012-04-25
关键词	物联网服务时间自动机环境实体服务建模模型验证
中文摘要	物联网服务的建模和验证是当前物联网服务提供中的一个重要问题.文中将物联网服务的行为建模为其与相关环境实体的交互,并引入环境实体以刻画物理世界各种物体的属性和行为,从而将物联网服务能力建模为它能够导致的环境实体发生的期望变化.文中以时间自动机为建模工具,分别为将要监测和要控制的物理环境实体以及不同种类的物联网服务独立建模,以表现它们的独立性和自主性.这些时间自动机形成一个网络,刻画完整的物联网服务的通信并发过程,物联网服务的实施过程表现为时间自动机网络上的状态变迁通路.最后,文中提出一组物联网服务要满足的性质,并利用模型检测工具UPPAAL验证物联网服务的正确性.
语种	中文
其他责任者	中国科学院数学与系统科学研究院 ; 中国科学院研究生院 ; 高可信软件技术教育部重点实验室(北京大学)
内容类型	期刊论文
源URL	[http://ir.calis.edu.cn/hdl/211010/4592]
专题	北京大学
推荐引用方式 GB/T 7714	李力行,金芝,李戈. 基于时间自动机的物联网服务建模和验证[J]. http://epub.edu.cnki.net/grid2008/brief/detailj.aspx?filename=JSJX201108004&dbname=CJFQ2011,2012, 2012.
APA	李力行,金芝,&李戈.(2012).基于时间自动机的物联网服务建模和验证.http://epub.edu.cnki.net/grid2008/brief/detailj.aspx?filename=JSJX201108004&dbname=CJFQ2011.
MLA	李力行,et al."基于时间自动机的物联网服务建模和验证".http://epub.edu.cnki.net/grid2008/brief/detailj.aspx?filename=JSJX201108004&dbname=CJFQ2011 (2012).