一种基于时间自动机的三余度飞控系统安全性分析方法

本发明属于民机飞控系统验证的技术领域，具体涉及一种基于时间自动机的三余度飞控系统安全性分析方法。包括：确定各个组件的时钟周期和随机漂移范围；采用时间自动机和三余度飞控系统的组件的时钟周期和随机漂移范围构造时钟模型，其中时间自动机的建模语义包括：location、guard、invariant和channel；基于三余度飞控系统的架构和时钟模型，构造基于时间自动机的三余度飞控系统的形式化模型；在基于时间自动机的三余度飞控系统的形式化模型的基础上构造故障模型，故障包括死机、总线传输和瞬时故障；对三余度飞控系统进行安全性分析，获取基于三余度飞控系统的安全性属性，并表达为形式化规约；采用形式化验证工具验证故障模型是否满足形式化规约。