一种基于UPPAAL的MeshCoP协议解耦建模和组合验证方法

本发明公开了一种基于UPPAAL的MeshCoP协议解耦建模和组合验证方法，包括：将MeshCoP协议的入网流程划分为多个相对独立的子阶段，并抽象出各子阶段建模所需要的变量、通道、函数；在UPPAAL中为各子阶段分别建模，每个模型均由多个自动机并发组合而成，每个自动机对应MeshCoP协议中的一个角色；对各个子阶段的模型进行形式化性质验证，判断各个模型的内部性质是否成立；基于各子阶段已验证的性质，对各子阶段的模型进一步抽象，形成各子阶段的自动机模型；集成各子阶段的自动机模型，组合构建MeshCoP协议的综合模型；基于构建的MeshCoP协议的综合模型，验证MeshCoP协议跨阶段的全局性质。