基于程序转化的SCADE模型检测  

SCADE Model Checking Based on Program Transformation

作　　者：冉丹 陈哲[1,2,3] 孙毅 杨志斌 RAN Dan;CHEN Zhe;SUN Yi;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

出　　处：《计算机科学》2021年第12期125-130,共6页Computer Science

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

摘　　要：SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码。目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后。为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测。此外,通过理论推导和大量实验证明了工具的模型检测的正确性。实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低。SCADE synchronization language is a common programming language for embedded system.It is often used to realize real-time embedded automatic control system in the research of equipment in aviation,aerospace,transportation and other safety critical fields.SCADE synchronization language is derived from the Lustre language,which adds more language structure to simplify source code.However,compared with Lustre language,the development of model checking technology of SCADE synchronous language is relatively backward.In this paper,we introduce a method and suite for model checking of SCADE programs.The core idea of the method is based on program transformation,that is,the SCADE program is finally transformed into equivalent Lustre program after lexical analysis,syntax analysis,abstract syntax tree generation,simplification,and then use JKind to complete the model checking.Moreover,we prove the correctness of the suite’s model checking result by theoretical deduction and a large number of experiments.Experimental results show that the SCADE and Lustre programs with the same function produce the same model checking results,but the efficiency of SCADE is lower.

关 键 词：模型检测 安全有限状态机 词法分析 语法分析 抽象语法树 JKind 

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