Computer Science

Computer Science ›› 2021, Vol. 48 ›› Issue (12): 125-130.doi: 10.11896/jsjkx.201100080

• Computer Software • Previous Articles     Next Articles

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).

PDF (PC)

828

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

CLC Number: 

  • 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] CHANG Jian-ming, BO Li-li, SUN Xiao-bing. Code Search Engine for Bug Localization [J]. Computer Science, 2021, 48(12): 140-148.
[2] HAN Lei, HU Jian-peng. Deduplication Algorithm of Abstract Syntax Tree in GCC Based on Trie Tree of Keywords [J]. Computer Science, 2020, 47(9): 47-51.
[3] DING Rong, YU Qian-hui. Growth Framework of Autonomous Unmanned Systems Based on AADL [J]. Computer Science, 2020, 47(12): 87-92.
[4] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[5] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[6] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[7] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[8] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[9] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[10] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[11] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[12] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[13] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[14] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[15] GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.