基于多引擎并行协作的 SCADE 模型检测

来源：计算机技术与发展杂志2023年第11期北京时间：

作者：方雨瑶;张聪

单位：南京航空航天大学 计算机科学与技术学院,江苏 南京 211106 Author(s): FANG Yu-yao;ZHANG Cong School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China 关键词: 同步语言;形式化验证;一阶逻辑;反应系统;可满足性模理论 Keywords: synchronous languages;formal verification;first-order logic;reactive systems;satisfiability mode theory 分类号: TP311 DOI: 10. 3969 / j. issn. 1673-629X. 2023. 11. 013 摘要: SCADE 语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。 已有的 SCADE 同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。 为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行 BMC 引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对 SCADE 同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题。 实现了一款针对 SCADE 同步语言程序的模型检测工具 PSMC,该工具采用多引擎并行协作方法来提升 SCADE 同步语言程序模型检测的效率。 手动构造了 887 个 SCADE 同步语言程序用于对 PSMC 进行实验验证,结果表明提出的优化方法可以有效地对 SCADE 同步语言程序进行自动的验证,并且可以提升模型检测的验证效率( 约 31% ) 。 Abstract: SCADE language is a synchronous data flow language that is commonly used for the development of real - time embeddedautomatic control systems and has a wide range?of applications in the aerospace, transportation and nuclear industries. The existingSCADE synchronous language model checking tools suffer from the inability to verify some?of the complex programs and the inefficiencyof verification. In order to solve the existing problems,we propose a multi-engine parallel collaboration approach,in which three?model　checking engines,namely the BMC engine,the induction engine and the program abstraction engine,are executed in parallel to collaborateon the verification of SCADE synchronous language programs,where the program abstraction engine solves the problem of inefficient verification of large complex programs by means of counterexample-guided abstraction refinement. We have implemented a model checkingtool,PSMC,for SCADE synchronous language programs, which uses a multi - engine parallel collaboration approach to improve theefficiency of model checking for SCADE synchronous language programs. We manually construct 887 SCADE synchronous languageprograms for experimental verification of PSMC, and the results show that the proposed optimization method can effectively andautomatically verify SCADE synchronous language programs, and can improve the verification efficiency of model checking byabout 31% .

摘要：SCADE 语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。 已有的 SCADE 同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。 为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行 BMC 引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对 SCADE 同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题。 实现了一款针对 SCADE 同步语言程序的模型检测工具 PSMC,该工具采用多引擎并行协作方法来提升 SCADE 同步语言程序模型检测的效率。 手动构造了 887 个 SCADE 同步语言程序用于对 PSMC 进行实验验证,结果表明提出的优化方法可以有效地对 SCADE 同步语言程序进行自动的验证,并且可以提升模型检测的验证效率( 约 31% ) 。

关键词：同步语言;形式化验证;一阶逻辑;反应系统;可满足性模理论