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

SCADE Model Checking Based on Multi-engine Parallel Collaboration

作　　者：方雨瑶 张聪[1] FANG Yu-yao;ZHANG Cong(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106

出　　处：《计算机技术与发展》2023年第11期86-90,共5页Computer Technology and Development

基　　金：国家自然科学基金(62172217);国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130);中央高校基本科研业务费人工智能+专项(NZ2020019)。

摘　　要：SCADE语言是一种同步数据流语言,通常被用于实时嵌入式自动控制系统的开发,在航空航天、交通、核工业等领域有广泛的应用。已有的SCADE同步语言模型检测工具存在无法验证部分复杂程序和验证效率低下的问题。为了解决现有的问题,该文提出了多引擎并行协作的方法,通过并行执行BMC引擎、归纳法引擎和程序抽象引擎三个模型检测引擎来实现对SCADE同步语言程序验证的协作,其中程序抽象引擎通过反例引导的抽象精化方法解决了大型复杂程序验证效率低下的问题。实现了一款针对SCADE同步语言程序的模型检测工具PSMC,该工具采用多引擎并行协作方法来提升SCADE同步语言程序模型检测的效率。手动构造了887个SCADE同步语言程序用于对PSMC进行实验验证,结果表明提出的优化方法可以有效地对SCADE同步语言程序进行自动的验证,并且可以提升模型检测的验证效率(约31%)。ion refinement.We have implemented a model checking tool,PSMC,for SCADE synchronous language programs,which uses a multi-engine parallel collaboration approach to improve the efficiency of model checking for SCADE synchronous language programs.We manually construct 887 SCADE synchronous language programs for experimental verification of PSMC,and the results show that the proposed optimization method can effectively and automatically verify SCADE synchronous language programs,and can improve the verification efficiency of model checking by about 31%.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]