基于程序切片和多属性增量验证的SCADE模型检测
方雨瑶
陈哲
南京航空航天大学计算机科学与技术学院 南京 211106
摘要：近年来安全关键控制系统领域由于软件故障造成的人员伤亡及经济损失等损害呈现逐年上升的趋势.SCADE同步语言作为被广泛应用于安全关键控制系统领域开发的语言在程序正确性验证上也越来越受重视.为了解决现有的SCADE同步语言模型检测工具验证效率低的问题,论文提出了一种基于程序切片和多属性增量检测的模型检测方法,该方法通过程序切片算法删除与属性无关的数据流和等式来简化被验证程序,通过多属性增量验证算法复用中间验证结果加快验证速度.最后实现了一款针对SCADE同步语言程序的模型检测工具,该工具在并行验证架构的基础上实现了优化算法以提升SCADE同步语言模型检测的效率.并且手动构造了887个SCADE同步语言程序用于对工具进行实验验证,结果表明论文提出的优化方法可以对SCADE同步语言程序进行有效的自动的验证,并且可以提升模型检测的验证效率约15%.
关键词：同步语言安全关键控制系统模型检测程序验证
分类号：TP311(计算技术、计算机技术)
资助基金：国家自然科学基金(62172217)国家自然科学基金(U1533130)中央高校基本科研业务费人工智能+专项(NZ2020019)
论文发表日期：2025-10-20
在线出版日期：2026-01-16（本平台首次上网日期，不代表文献的发表时间）
页数：6( 2728-2732,2823 )
英文信息