物联网服务的π-演算建模与验证

针对物联网服务建模和验证问题,用π-演算理论对物联网服务和环境实体进行动态交互行为建模,并引入μ-演算刻画物联网服务能力,将其描述为物联网服务和环境实体动态交互行为的执行序列。针对特定的应用场景,使用π-演算定义了物联网服务和环境实体,利用μ-演算对物联网服务能力进行建模,使用检测工具MWB验证了模型的安全性、活性和时间约束三个性质,为物联网服务建模和验证提供了参考。