计算机科学 ›› 2021, Vol. 48 ›› Issue (12): 125-130.doi: 10.11896/jsjkx.201100080

• 计算机软件 • 上一篇    下一篇

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

冉丹, 陈哲, 孙毅, 杨志斌   

  1. 南京航空航天大学计算机科学与技术学院 南京211106
    华东师范大学上海市高可信计算重点实验室 上海200062
    南京大学计算机软件新技术国家重点实验室 南京210093
  • 收稿日期:2020-11-09 修回日期:2021-04-12 出版日期:2021-12-15 发布日期:2021-11-26
  • 通讯作者: 陈哲(zhechen@nuaa.edu.cn)
  • 作者简介:RDan456@163.com
  • 基金资助:
    国家自然基金委员会-中国民航局民航联合研究基金(U1533130);中央高校基本科研业务费人工智能+专项(NZ2020019);上海市高可信计算重点实验室开放课题,南京大学计算机软件新技术国家重点实验室开放课(KFKT2020B10)

SCADE Model Checking Based on Program Transformation

RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin   

  1. 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
  • Received:2020-11-09 Revised:2021-04-12 Online:2021-12-15 Published:2021-11-26
  • About author:RAN Dan,born in 1996,postgraduate.His main research interests include veri-fication of software and model checking.
    CHEN Zhe,born in 1981,associate professor,is a member of China Computer Federation.His main research interests include verification of software,software engineering and network security.
  • Supported by:
    Joint Research Funds of National Natural Science Foundation of China and Civil Aviation Administration of China(U1533130),Fundamental Research Funds for AI(NZ2020019) and Open Project of Shanghai Key Laboratory of Trustworthy Computing,Open Project of State Key Laboratory for Novel Software Technology(KFKT2020B10).

摘要: SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码。目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后。为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测。此外,通过理论推导和大量实验证明了工具的模型检测的正确性。实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低。

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

Abstract: 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.

Key words: Model checking, Safe state machine, Lexical analysis, Syntax analysis, Abstract syntax tree, JKind

中图分类号: 

  • TP311
[1]YANG P,WANG S Y.Survey on Trustworthy Compilers for Synchronous Data-flow Languages[J].Computer Science,2019,46(5):21-28.
[2]YANG Z B,YUAN S H,XIE J,et al.Multi-threaded code ge- neration toolfor synchronous language[J].Journal of Software,2019,30(7):1980-2002.
[3]COLAÇO J L,PAGANO B,POUZET M.SCADE 6:A formal language for embedded critical software development[C]//2017 International Symposium on Theoretical Aspects of Software Engineering(TASE).IEEE,2017:1-11.
[4]DURAK U,D'AMBROGIO A,BOCCIARELLI P.Safety-critical simulation engineering[C]//Proceedings of the 2020 Summer Simulation Conference.2020:1-12.
[5]SIRJANI M,LEE E A,KHAMESPANAH E.Model checking software in cyberphysical systems[C]//2020 IEEE 44th Annual Computers,Software,and Applications Conference(COMPSAC).IEEE,2020:1017-1026.
[6]HAGEN G,TINELLI C.Scaling up the formal verification of Lustre programs with SMT-based techniques[C]//2008 Formal Methods in Computer-Aided Design.IEEE,2008:1-9.
[7]CHAMPION A,MEBSOUT A,STICKSEL C,et al.The kind 2 model checker[C]//International Conference on Computer Aided Verification.Cham:Springer,2016:510-517.
[8]KAHSAI T,TINELLI C.PKind:A parallel k-induction based model checker[J].Electronic Proceedings in Theoretical Computer Science,2011,72:55-62.
[9]GACEK A,BACKES J,WHALEN M,et al.The JKind model checker[C]//International Conference on Computer Aided Ve-rification.Cham:Springer,2018:20-27.
[10]BASOLD H,GÜNTHER H,HUHN M,et al.An open alternative for SMT-based verification of SCADE models[C]//International Workshop on Formal Methods for Industrial Critical Systems.Cham:Springer,2014:124-139.
[11]BARRETT C,TINELLI C.Satisfiability modulo theories[M]//Handbook of Model Checking.Cham:Springer,2018:305-343.
[12]AHO A V,SETHI R,ULLMAN J D.Compilers,principles, techniques[J].Adson Wesley,1986,7(8):9.
[13]NEAMTIU I,FOSTER J S,HICKS M.Understanding source code evolution using abstract syntax tree matching[C]//Proceedings of the 2005 International Workshop on Mining Software Repositories.2005:1-5.
[14]JOHN L.Flex & Bison:Text Processing Tools[M].O'Reilly Media,Inc:Cambridge,2009:1.
[15]HOPCROFT J E,MOTWANI R,ULLMAN J D.Introduction to automata theory,languages,and computation[J].Acm Sigact News,2001,32(1):60-65.
[16]ANDRÉ C.Semantics of SSM(safe state machine) [R].Technical Report,Esterel Technologies,2003.
[17]MCMILLAN K L.Symbolic model checking[M]//Symbolic Model Checking.Boston,MA:Springer,1993:25-60.
[18]DE MOURA L,RUEβ H,SOREA M.Bounded model checking and induction:From refutation to verification[C]//International Conference on Computer Aided Verification.Berlin:Springer,2003:14-26.
[1] 常建明, 薄莉莉, 孙小兵. 面向缺陷定位的代码搜索引擎[J]. 计算机科学, 2021, 48(12): 140-148.
[2] 韩磊, 胡建鹏. 基于关键词Trie树的GCC抽象语法树消除冗余算法[J]. 计算机科学, 2020, 47(9): 47-51.
[3] 骆翔宇, 许杭娜, 曾昊晟, 陈祖希, 杨帆. 离散实时线性动态逻辑的符号化模型检测[J]. 计算机科学, 2020, 47(9): 204-212.
[4] 李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程[J]. 计算机科学, 2020, 47(6): 8-15.
[5] 丁嵘, 于千惠. 基于AADL的自主无人系统可成长框架[J]. 计算机科学, 2020, 47(12): 87-92.
[6] 蔡泳, 钱俊彦, 潘海玉. 基于度量线性时态逻辑的近似安全性[J]. 计算机科学, 2020, 47(10): 309-314.
[7] 夏奴奴, 杨晋吉, 赵淦森, 莫晓珊. 基于概率模型的云辅助的轻量级无证书认证协议的形式化验证[J]. 计算机科学, 2019, 46(8): 206-211.
[8] 韩英杰, 周清雷, 朱维军. 基于DNA计算的计算树逻辑模型检测方法研究进展[J]. 计算机科学, 2019, 46(11): 25-31.
[9] 周女琪, 周宇. 基于概率模型检测的Web服务组合多目标验证[J]. 计算机科学, 2018, 45(8): 288-294.
[10] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71-75.
[11] 聂凯,周清雷,朱维军,张朝阳. 基于时序逻辑的3种网络攻击建模[J]. 计算机科学, 2018, 45(2): 209-214.
[12] 杨红, 洪玫, 屈媛媛. 基于模型检测技术的变异测试用例生成方法[J]. 计算机科学, 2018, 45(11A): 488-493.
[13] 赵莹, 潘华, 张云猛, 莫启, 代飞. 协同业务过程建模与行为验证[J]. 计算机科学, 2018, 45(11A): 597-602.
[14] 刘爽, 魏欧, 郭宗豪. 基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制[J]. 计算机科学, 2018, 45(10): 313-319.
[15] 杜伊,何洋,洪玫. 概率模型检测在动态能耗管理中的应用[J]. 计算机科学, 2018, 45(1): 261-266.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 李贵,陈盛红,李征宇,韩子阳,孙平. 融合用户时效偏好的推荐算法[J]. 计算机科学, 2014, 41(Z6): 394 -399 .
[2] 高蕾,胡玉鹏. WSN中基于最小延时的数据汇集树构建与传输调度算法[J]. 计算机科学, 2017, 44(Z6): 300 -304 .
[3] 朱焱. 万维网资源质量模式挖掘技术分析[J]. 计算机科学, 2010, 37(8): 201 -207 .
[4] 汪晓妍, 刘琪琪, 黄晓洁, 姜娓娓, 夏明. 基于空间对齐和轮廓匹配的颈动脉多对比MRI三维配准方法[J]. 计算机科学, 2019, 46(5): 241 -246 .
[5] 韩佳佳, 张德平. 考虑软件运行的软-硬件退化系统剩余寿命估计[J]. 计算机科学, 2019, 46(6A): 511 -517 .
[6] 黄虹玮,刘玉娇,沈卓恺,张少伟,陈志敏,高阳. 基于深度学习网络模型的端到端航迹关联[J]. 计算机科学, 2020, 47(3): 200 -205 .
[7] 孟利民, 王锟, 郑增乾, 蒋维. 基于粒子群算法的D2D内容边缘缓存架构策略[J]. 计算机科学, 2020, 47(11A): 345 -348 .
[8] 潘孝勤, 芦天亮, 杜彦辉, 仝鑫. 基于深度学习的语音合成与转换技术综述[J]. 计算机科学, 2021, 48(8): 200 -208 .
[9] 王俊, 王修来, 庞威, 赵鸿飞. 面向科技前瞻预测的大数据治理研究[J]. 计算机科学, 2021, 48(9): 36 -42 .
[10] 余力, 杜启翰, 岳博妍, 向君瑶, 徐冠宇, 冷友方. 基于强化学习的推荐研究综述[J]. 计算机科学, 2021, 48(10): 1 -18 .