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

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