一种SCADE同步语言程序安全属性自动验证工具  

Tool for Automatically Verify Safety Properties of SCADE Programs

作　　者：孙毅 陈哲[1,2,3] 冉丹 杨志斌 SUN Yi;CHEN Zhe;RAN Dan;YANG Zhi-bin(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China;State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]华东师范大学上海市高可信计算重点实验室,上海200062 [3]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《小型微型计算机系统》2022年第4期858-864,共7页Journal of Chinese Computer Systems

基　　金：国家自然基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;中央高校基本科研业务费人工智能+专项项目(NZ2020019)资助;南京大学计算机软件新技术国家重点实验室开放课题项目(KFKT2020B10)资助。

摘　　要：安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可将SCADE同步语言程序的安全属性的验证问题转化为无量词一阶逻辑公式的可满足性问题;然后采用先进的可满足性模理论求解器对其可满足性进行求解.本方法旨在实现对SCADE同步语言程序进行自动地、直接地验证,以填补SCADE同步语言程序验证领域的技术空白.此外,本文对所提方法进行了代码实现,并通过实验验证了所提方法的有效性.Reactive systems in safety-critical fields are mostly developed using synchronous languages.However,there is no formal verification tool for SCADE programs in academia.In this paper,we proposea method to verify the safety properties of SCADE programs automatically.Firstly,we use the quantifier-free first-order logic formula to model the behavior of the SCADE program,and then convert the verification problem of the safety propertiesin SCADE program into the satisfiability problem of the quantifier-free first-order logic formula.Finally,we use the SMT solver to solve the satisfiability.This methodcan realize the verification of SCADE programs automatically and directly,so as to fill the technical gap in the field of SCADE program verification.Moreover,we implement the proposed method in code,and experimental resultshow that the proposed method is effective.

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

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