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

发布时间：2023-04-02 09:11

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

【文章页数】：7 页

【文章目录】：
0 引言
1 基于时空I/O混成自动机的物联网服务建模与验证的框架
    1.1 一个物联网典型应用场景
    1.2 物联网服务
    1.3 时空I/O混成自动机
        1.3.1混成自动机
        1.3.2 时空I/O混成自动机的定义
    1.4 物联网实体和服务模型
    1.5 基于时空I/O混成自动机的物联网服务建模与验证框架
2 基于时空I/O混成自动机的物联网服务建模
    2.1 描述物联网服务
    2.2 基于时空I/O混成自动机的物联网服务模型
    2.3基于时空I/O混成自动机的物联网服务建模
3 微分动态逻辑验证方法与Hybrid Program
    3.1 微分动态逻辑
    3.2 微分动态逻辑模型
4 案例验证
    4.1 模型的验证
    4.2 验证和分析
5 结束语



本文编号：3778961