一种基于分布式实时双余度系统形式化建模与验证方法

本发明属于分布式实时双余度系统验证技术领域，具体涉及一种基于分布式实时双余度系统形式化建模与验证方法。包括：步骤1：分析分布式实时双余度系统的架构，分解出系统架构的所有时钟；步骤2：基于各时钟的晶振频率和漂移，确定相应时钟的周期和随机漂移范围；步骤3：采用形式化语义，基于步骤2中确定的时钟的周期和随机漂移范围构造时钟模型；步骤4：基于分布式实时双余度系统的架构的功能逻辑构造分布式实时双余度系统的功能逻辑的形式化模型，并在此基础上叠加步骤3中形成的时钟模型构造分布式实时双余度系统的形式化模型；步骤5：对分布式实时双余度系统进行安全性分析，获得安全性属性，基于安全性属性进行形式化验证。