【摘要】 物联网服务的建模和验证是物联网研究中的重要问题。文中对混成自动机进行了扩展,提出了具有位置驱动特点的时空I/O混成自动机。文中提出了基于时空I/O混成自动机的物联网服务建模与验证框架。在框架中,首先对物联网服务进行了描述,并使用时空I/O混成自动机对物联网服务进行建模。这些时空I/O混成自动机形成一个网络,刻画完整的物联网服务的通信并行过程。文中采用的形式化验证方法为微分动态逻辑(Differential Dynamic Logic,DL),其操作模型为HP(Hybrid Program)。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的物联网服务性质进行规约,最后使用定理证明器KeYmaera验证物联网服务的正确性。更多还原

【Abstract】 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.更多还原