Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (12): 73-86.doi: 10.11896/jsjkx.190400035

Special Issue: Software Engineering & Requirements Engineering for Complex Systems

Previous Articles     Next Articles

Transformation Method for AltaRica3.0 Model to NuSMV Model

CHEN Shuo1,2, HU Jun1,2, TANG Hong-ying1, SHI Meng-ye1   

  1. 1 College of Computer Science and Technology Nanjing University of Aeronautics and Astronautics Nanjing 211106,China
    2 Collaborative Innovation Center of Novel Software Technology and Industrialization Nanjing 210007,China
  • Received:2019-04-08 Revised:2019-08-04 Online:2020-12-15 Published:2020-12-17
  • About author:CHEN Shuo,born in 1996is currently pursuing the M.E.degree.His main research interests include intelligent computing and analysis for advanced systemsmodel-based systems engineeringsystem safety modeling and analysis.
    HU Jun,born in 1973Ph.Dassociate professoris a senior member of China Computer Federation.His main research interests include intelligent computing and analysis for advanced systemsmodel-based systems engineeringsystem safety modeling and analysis.
  • Supported by:
    National Basic Research Program of China (973 Program) (2014CB744904) and Foundation of Graduate Innovation Centre in Nanjing University of Aeronautics and Astronautics(kfjj20181607).

PDF (PC)

996

Abstract: AltaRica 3.0 is a safety modeling and analysis language for safety-critical systems.Because AltaRica 3.0 lacks model checking techniques for temporal properties and does not support exhaustive spaceexaminationNuSMV supports exhaustive model checking techniques.This paper expands AltaRica 3.0proposes the transformation rules and algorithms of the AltaRica 3.0 model to the NuSMV model based on the language parser generator ANTLR (Another Tool for Language Recognition).FirstlyASTLR is used to construct the AST (Abstract Syntax Tree) of the AltaRica 3.0 flattening GTS model.Secondlythe language structure transformation rules are designed to show the behavioral semantic correspondence between AltaRica 3.0 and NuSMV.Thenwe design the transformation algorithm G2N.When traversing the ASTG2N acquires and transforms the GTS model language information stored by the nodeand obtains the transformed NuSMV file through the continuous traversal transformation process while ensuring semantic retention.Finallyexample of four typical cases in requirement engineering are used for experimental analysis to verify the effectiveness of the G2N and the safety of the requirement model.Experiments show that the G2N algorithm can complete the conversion of AltaRica 3.0 model to NuSMV model at lexical and grammatical level.

Key words: AltaRica 3.0, ANTLR, AST, GTS, Model transform, NuSMV

CLC Number: 

  • TP311
[1] CHENG C,LIU Y F.Research on Model Based Safety Analysis[J].Advances in Aeronautical Science And Engineering,2016,7(3):369-373.
[2] GOMES A,MOTA A,SAMPAIO A,et al.Systematic Model-Based Safety Assessment Via Probabilistic Model Checking[M]//Leveraging Applications of Formal Methods,Verification and Validation.2010:625-639.
[3] SANGO M,VALLÉE F,VIÉ A C,et al.MBSE and MBSA with Capella and Safety Architect Tools[M]//Complex Systems Design &Management.2017.
[4] BOZZANO M,CIMATTI A,LISAGOR O,et al.Safety assessment of AltaRica models via symbolic model checking[J].Science of Computer Programming,2015,98(4):464-483.
[5] GRIFFAULT A,VINCENT A.The Mec 5 model-checker[C]//International Conference on Computer Aided Verification.Springer,2004.
[6] BOITEAU M,DUTUIT Y,RAUZY A,et al.The AltaRica data-flow language in use:modeling of production availability of a multi-state system[J].Reliability Engineering &System Safety,2006,91(7):747-755.
[7] RUIN T,IUNG B,DESPUJOLS A,et al.Complex maintenance programs quantification (CMPQ) to better control production systems[J].Journal of Manufacturing Technology Management,2014,25(4):491-509.
[8] ArNOLD A,POINT G,GRIFFAULT A,et al.The AltaRica Formalism for Describing Concurrent Systems[J].Fundamenta Informaticae,1999,40(2/3):109-124.
[9] GRIFFAULT A,POINT G,KUNTZ F,et al.Symbolic computation of minimal cuts for AltaRica models[R].Talence Cedex,France:LaBRI,Université de Bordeaux,2011.
[10] YONG J,QIU Z.S2N:Model Transformation from SPIN toNuSMV[C]//International Conference on Model Checking Software.2012.
[11] ZHOU Y P.Research on Safety Analysis of Train Control System in Requirements Phase Based on UML-NuSMV Model[D].Beijing:Beijing Jiaotong University,2015.
[12] LI Y,CAO Z N.Investigation on Formal Modeling and Verification Method Based on Specification[J].Computer Technology And Development,2017,27(6):7-10.
[13] LIU K,YANG H L,LIAO H S,et al.Xml Schema Constraints Extraction Based on Model Checking[J].Computer Applications and Software,2012(11):160-164.
[14] ZHANG T,XIE H,HUANG S B.The Method of Model Checking Policy of Multi-Agent Interaction[J].Journal of University of Electronic Science and Technology of China,2016,45(5):802-807.
[15] SZPYRKA M,BIERNACKA A,BIERNACKI J.Methods ofTranslation of Petri Nets to NuSMV Language[C]//CS&P.2014.
[16] ARCAINI P,GARGANTINI A,RICCOBENE E.AsmetaSMV:a way to link high-level ASM models to low-level NuSMV specifications[C]//International Conference on Abstract State Machines.Springer,2010.
[17] CALTAIS G,LEITNER-FISCHER F,LEUE S,et al.SysML to NuSMV Model Transformation via Object-Orientation[C]//International Workshop on Design.2016.
[18] LAM V S.Formal analysis of BPMN models:a NuSMV-based approach[J].International Journal of Software Engineering and Knowledge Engineering,2010,20(7):987-1023.
[19] JUN H,SONG C,MINGMING W.A Transformation Method for AltaRica 3.0 to Promela and Its Verification[J].Computer Engineering &Science,2017,39(4):708-716.
[20] CIMATTI A,MOVER S,TONETTA S.HyDI:A Language for Symbolic Hybrid Systems with Discrete Interaction[C]//Euromicro Conference on Software Engineering &Advanced Applications.2011.
[21] PARR T.The Definitive ANTLR 4 Reference[M].PragmaticBookshelf,2013:184.
[22] QUONG R W.ANTLR:A Predicated-LL(k) Parser Generator[J].Software Practice &Experience,2010,25(7):789-810.
[23] PROSVIRNOVA T,RAUZY A.Guarded transition systems:Pivot modelling formalism for safety analysis[C]//Actes du Congres Lambda-Mu.2012.
[24] PROSVIRNOVA T.AltaRica 3.0:a Model-Based approach for Safety Analyses[D].Paris:Ecole Polytechnique.2014.
[25] CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.NUSMV:a new symbolic model checker[J].International Journal on Software Tools for Technology Transfer,2000,2(4):410-425.
[26] CIMATTI A,CLARKE E,GIUNCHIGLIA E,et al.NuSMV 2:An OpenSource Tool for Symbolic Model Checking[M]//Computer Aided Verification.Berlin:Springer,2002.
[27] STEWART D,WHALEN M W,COFER D,et al.Architectural Modeling and Analysis for Safety Engineering[C]//International Symposium on Model-Based Safety and Assessment.2017.
[28] MORTADA H,PROSVIRNOVA T,RAUZY A.Safety Assessment of an Electrical System with AltaRica 3.0[M]//Model-Based Safety and Assessment.Cham:Springer,2014.
[1] LIU Xin, WANG Jun, SONG Qiao-feng, LIU Jia-hao. Collaborative Multicast Proactive Caching Scheme Based on AAE [J]. Computer Science, 2022, 49(9): 260-267.
[2] LIU Dong-mei, XU Yang, WU Ze-bin, LIU Qian, SONG Bin, WEI Zhi-hui. Incremental Object Detection Method Based on Border Distance Measurement [J]. Computer Science, 2022, 49(8): 136-142.
[3] YANG Xiao, WANG Xiang-kun, HU Hao, ZHU Min. Survey on Visualization Technology for Equipment Condition Monitoring [J]. Computer Science, 2022, 49(7): 89-99.
[4] SHAO Xin-xin. TI-FastText Automatic Goods Classification Algorithm [J]. Computer Science, 2022, 49(6A): 206-210.
[5] ZHU Wen-tao, LAN Xian-chao, LUO Huan-lin, YUE Bing, WANG Yang. Remote Sensing Aircraft Target Detection Based on Improved Faster R-CNN [J]. Computer Science, 2022, 49(6A): 378-383.
[6] ZHAO Ming-hua, ZHOU Tong-tong, DU Shuang-li, SHI Zheng-hao. Single Backlit Image Enhancement Based on Virtual Exposure Method [J]. Computer Science, 2022, 49(6A): 384-389.
[7] XU Jie, ZHU Yu-kun, XING Chun-xiao. Application of Machine Learning in Financial Asset Pricing:A Review [J]. Computer Science, 2022, 49(6): 276-286.
[8] LU Ting, HOU Guo-jia, PAN Zhen-kuan, WANG Guo-dong. Underwater Image Quality Assessment Based on HVS [J]. Computer Science, 2022, 49(5): 98-104.
[9] WANG Ben-yu, GU Yi-jun, PENG Shu-fan, ZHENG Di-wen. Community Detection Algorithm Based on Dynamic Distance and Stochastic Competitive Learning [J]. Computer Science, 2022, 49(5): 170-178.
[10] GUO Si-yu, WU Yan-dong. Improved Ellipse Fitting Algorithm with Outlier Removal [J]. Computer Science, 2022, 49(4): 188-194.
[11] XIE Yu, YANG Rui-ling, LIU Gong-xu, LI De-yu, WANG Wen-jian. Human Skeleton Action Recognition Algorithm Based on Dynamic Topological Graph [J]. Computer Science, 2022, 49(2): 62-68.
[12] WANG Jun, WANG Xiu-lai, PANG Wei, ZHAO Hong-fei. Research on Big Data Governance for Science and Technology Forecast [J]. Computer Science, 2021, 48(9): 36-42.
[13] CHENG Zhao-wei, SHEN Hang, WANG Yue, WANG Min, BAI Guang-wei. Deep Reinforcement Learning Based UAV Assisted SVC Video Multicast [J]. Computer Science, 2021, 48(9): 271-277.
[14] ZHANG Jie, YUE Shao-hua, WANG Gang, LIU Jia-yi, YAO Xiao-qiang. Multi-agent System Based on Stackelberg and Edge Laplace Matrix [J]. Computer Science, 2021, 48(8): 253-262.
[15] FANG Ting, GONG Ao-yu, ZHANG Fan, LIN Yan, JIA Lin-qiong, ZHANG Yi-jin. Dynamic Broadcasting Strategy in Cognitive Radio Networks Under Delivery Deadline [J]. Computer Science, 2021, 48(7): 340-346.
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.