计算机科学 ›› 2021, Vol. 48 ›› Issue (12): 125-130.doi: 10.11896/jsjkx.201100080
冉丹, 陈哲, 孙毅, 杨志斌
RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin
摘要: SCADE同步语言是一种常用的嵌入式系统程序设计语言。在航空、航天、交通等安全关键领域的装备研发中,SCADE同步语言通常被用于实现实时嵌入式自动控制系统。SCADE语言是工业级的开发工具,它源于Lustre语言,并在其基础上增加了更多的语言结构来精简代码。目前,相比Lustre语言,SCADE程序模型检测的学术研究相对落后。为此,文中提出了一种对SCADE程序进行模型检测的方法并实现了一款SCADE模型检测工具,该方法的核心思想是基于程序转化,即把SCADE程序经过词法分析、语法分析、抽象语法树生成与化简等操作最终转化为等价的Lustre程序,然后用JKind与SMT求解器完成模型检测。此外,通过理论推导和大量实验证明了工具的模型检测的正确性。实验结果表明,功能相同的两个SCADE和Lustre测试用例模型的检测结果相同,但SCADE程序的模型检测效率相对较低。
中图分类号:
[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 |
|