基于时空I/O混成自动机的物联网服务验证  

Modeling and Verification Services of Internet of Things Based on Spatial I/O Hybrid Automata

作　　者：赵文明[1] 张敏[2] 

机构地区：[1]杭州职业技术学院信息电子系,杭州310018 [2]华东师范大学上海市高可信计算重点实验室,上海200062

出　　处：《科技通报》2014年第5期95-101,共7页Bulletin of Science and Technology

基　　金：国家自然科学基金项目(61061130541);国家自然科学基金项目(61202105);国家"973"重点基础研究发展计划项目基金(2011CB302802);985平台项目"085知识创新工程"

摘　　要：物联网服务的建模和验证是物联网研究中的重要问题。文中对混成自动机进行了扩展,提出了具有位置驱动特点的时空I/O混成自动机。文中提出了基于时空I/O混成自动机的物联网服务建模与验证框架。在框架中,首先对物联网服务进行了描述,并使用时空I/O混成自动机对物联网服务进行建模。这些时空I/O混成自动机形成一个网络,刻画完整的物联网服务的通信并行过程。文中采用的形式化验证方法为微分动态逻辑(Differential Dynamic Logic,DL),其操作模型为HP(Hybrid Program)。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的物联网服务性质进行规约,最后使用定理证明器KeYmaera验证物联网服务的正确性。The Modeling and Verifying of Internet of Things （IOT） service are now important aspects of IOT research. The Spatial I/O Hybrid Automata （SIOHA）, characteristic of the location-triggered, is proposed based on the extended hybrid automata. This paper presents a framework of IOT services modeling and verification based on SIOHA, where IOT services are modeled by SIOHA. All these SIOHA come into a network that represents the communication and parallelism of the whole IOT system. The adopted formal method is the differential dynamic logic （DL）, whose operational model is Hybrid Program （HP）. The SIOHA model is transformed to its corresponding HP through DL. Then IOT services property is specified based on the result from HP. Finally, the IOT services property is automatically verified through the theorem-prover named KeYmaera.

关 键 词：物联网服务 时空I O混成自动机 微分动态逻辑 时空一致性 形式化验证 KeYmaera 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]