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

作者：赵文明; 张敏

来源：科技通报, 2014, 30(05): 95-101.

DOI：10.13774/j.cnki.kjtb.2014.05.017

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

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

• 单位
  杭州职业技术学院; 华东师范大学