计算机科学 ›› 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: Abstract syntax tree, JKind, Lexical analysis, Model checking, Safe state machine, Syntax analysis

中图分类号: 

  • 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] 常建明, 薄莉莉, 孙小兵.
面向缺陷定位的代码搜索引擎
Code Search Engine for Bug Localization
计算机科学, 2021, 48(12): 140-148. https://doi.org/10.11896/jsjkx.201100209
[2] 韩磊, 胡建鹏.
基于关键词Trie树的GCC抽象语法树消除冗余算法
Deduplication Algorithm of Abstract Syntax Tree in GCC Based on Trie Tree of Keywords
计算机科学, 2020, 47(9): 47-51. https://doi.org/10.11896/jsjkx.190600042
[3] 李凌, 李璜华, 王生原.
在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程
Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design
计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173
[4] 丁嵘, 于千惠.
基于AADL的自主无人系统可成长框架
Growth Framework of Autonomous Unmanned Systems Based on AADL
计算机科学, 2020, 47(12): 87-92. https://doi.org/10.11896/jsjkx.201100173
[5] 蔡泳, 钱俊彦, 潘海玉.
基于度量线性时态逻辑的近似安全性
Approximate Safety Properties in Metric Linear Temporal Logic
计算机科学, 2020, 47(10): 309-314. https://doi.org/10.11896/jsjkx.191000175
[6] 夏奴奴, 杨晋吉, 赵淦森, 莫晓珊.
基于概率模型的云辅助的轻量级无证书认证协议的形式化验证
Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model
计算机科学, 2019, 46(8): 206-211. https://doi.org/10.11896/j.issn.1002-137X.2019.08.034
[7] 韩英杰, 周清雷, 朱维军.
基于DNA计算的计算树逻辑模型检测方法研究进展
Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking
计算机科学, 2019, 46(11): 25-31. https://doi.org/10.11896/jsjkx.181102091
[8] 周女琪, 周宇.
基于概率模型检测的Web服务组合多目标验证
Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking
计算机科学, 2018, 45(8): 288-294. https://doi.org/10.11896/j.issn.1002-137X.2018.08.052
[9] 雷丽晖,王静.
可能性测度下的LTL模型检测并行化研究
Parallelization of LTL Model Checking Based on Possibility Measure
计算机科学, 2018, 45(4): 71-75. https://doi.org/10.11896/j.issn.1002-137X.2018.04.010
[10] 聂凯,周清雷,朱维军,张朝阳.
基于时序逻辑的3种网络攻击建模
Modeling for Three Kinds of Network Attacks Based on Temporal Logic
计算机科学, 2018, 45(2): 209-214. https://doi.org/10.11896/j.issn.1002-137X.2018.02.036
[11] 杨红, 洪玫, 屈媛媛.
基于模型检测技术的变异测试用例生成方法
Approach of Mutation Test Case Generation Based on Model Checking
计算机科学, 2018, 45(11A): 488-493.
[12] 赵莹, 潘华, 张云猛, 莫启, 代飞.
协同业务过程建模与行为验证
Modeling and Behavior Verification for Collaborative Business Processes
计算机科学, 2018, 45(11A): 597-602.
[13] 刘爽, 魏欧, 郭宗豪.
基于概率模型检测和遗传算法的基因调控网络的无限范围优化控制
Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm
计算机科学, 2018, 45(10): 313-319. https://doi.org/10.11896/j.issn.1002-137X.2018.10.058
[14] 杜伊,何洋,洪玫.
概率模型检测在动态能耗管理中的应用
Application of Probabilistic Model Checking in Dynamic Power Management
计算机科学, 2018, 45(1): 261-266. https://doi.org/10.11896/j.issn.1002-137X.2018.01.046
[15] 曾赛文,文中华,戴良伟,袁润.
基于不确定攻击图的攻击路径的网络安全分析
Analysis of Network Security Based on Uncertain Attack Graph Path
计算机科学, 2017, 44(Z6): 351-355. https://doi.org/10.11896/j.issn.1002-137X.2017.6A.080
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!