摘要
SCADE语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用.已有的SCADE同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题.为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行BMC引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对SCADE同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题.实现了一款针对SCADE同步语言程序的模型检测工具PSMC,该工具采用多引擎并行协作方法来提升SCADE同步语言程序模型检测的效率.手动构造了887 个SCADE同步语言程序用于对PSMC进行实验验证,结果表明提出的优化方法可以有效地对SCADE同步语言程序进行自动的验证,并且可以提升模型检测的验证效率(约31%).
基金项目
国家自然科学基金(62172217)
国家自然科学基金-中国民用航空总局联合资助项目(U1533130)
中央高校基本科研业务费专项(NZ2020019)
国家科技期刊平台
NSTL
维普
万方数据