基于SMT的区域控制器同步反应式模型的形式化验证

李腾飞孙军峰吕新军陈祥刘静孙海英何积丰

卡斯柯信号有限公司; 华东师范大学;

摘要：

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序…展开v

关键词：形式化验证、安全关键系统、同步反应式模型、高阶迭代、程序转换

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家重点研发计划;国家自然科学基金;上海市超级博士后基金项目

在线出版日期：2023-07-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共19页

页码：3080-3098