计算机科学 ›› 2020, Vol. 47 ›› Issue (12): 73-86.doi: 10.11896/jsjkx.190400035
所属专题： 复杂系统的软件工程和需求工程
陈朔1,2, 胡军1,2, 唐红英1, 石梦烨1
CHEN Shuo1,2, HU Jun1,2, TANG Hong-ying1, SHI Meng-ye1
摘要： Alta Rica3.0是一类面向复杂关键系统的安全性建模与分析语言缺乏时态属性的模型检验技术不支持穷尽式的空间检验而Nu SMV支持穷尽式的模型检验技术因此对Alta Rica3.0模型进行扩展提出了基于语言解析器生成器ANTLR(Another Tool for Language Recognition)的Alta Rica3.0模型到NuSMV模型的转换规则和算法.首先利用ANTLR构建Alta Rica3.0平展化GTS模型的AST(Abstract Syntax Tree);其次设计语言结构转换规则显示Alta Rica3.0和NuSMV之间的行为语义对应关系;然后设计转换算法G2N在遍历AST时G2N对结点存储的GTS模型语言信息进行获取和转换在保留语义的情况下通过不断地遍历转换过程来获取转换后的Nu SMV文件;最后以需求工程中的4个典型案例为例进行实验分析验证了G2N的有效性和需求模型的安全性.实验结果表明G2N算法可以在词法和语法层次上完成AltaRica3.0模型到Nu SMV模型的转换工作.
中图分类号:
| [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] | 邵欣欣. TI-FastText自动商品分类算法 TI-FastText Automatic Goods Classification Algorithm 计算机科学, 2022, 49(6A): 206-210. https://doi.org/10.11896/jsjkx.210500089 |
| [2] | 祝文韬, 兰先超, 罗唤霖, 岳彬, 汪洋. 改进Faster R-CNN的光学遥感飞机目标检测 Remote Sensing Aircraft Target Detection Based on Improved Faster R-CNN 计算机科学, 2022, 49(6A): 378-383. https://doi.org/10.11896/jsjkx.210300121 |
| [3] | 祁健, 胡军, 谷青范, 荣灏, 展万里, 董彦宏. 一种AltaRica 3.0模型中类的平展化方法 Class Flattening Method for AltaRica 3.0 Model 计算机科学, 2021, 48(5): 51-59. https://doi.org/10.11896/jsjkx.200700184 |
| [4] | 展万里, 胡军, 谷青范, 荣灏, 祁健, 董彦宏. 基于模型的故障树自动生成方法 Model-based Fault Tree Automatic Generation Method 计算机科学, 2021, 48(12): 159-169. https://doi.org/10.11896/jsjkx.200800177 |
| [5] | 於志勇, 林力强, 陈艳, 周天, 倪一涛, 陈星. 面向Hyperledger Fabric的SQL访问框架 SQL Access Framework for Hyperledger Fabric 计算机科学, 2021, 48(11): 54-61. https://doi.org/10.11896/jsjkx.210100220 |
| [6] | 李思洁, 魏欧, 战芸娇, 王立松. 基于表格表达式的SCR需求模型转换 SCR Requirement Model Transformation Based on Table Expression 计算机科学, 2019, 46(6): 180-188. https://doi.org/10.11896/j.issn.1002-137X.2019.06.027 |
| [7] | 胡海根, 周莉莉, 周乾伟, 陈胜勇, 张俊康. 基于CNN的相衬显微图像序列的癌细胞多目标跟踪 Multi-target Tracking of Cancer Cells under Phase Contrast Microscopic Images Based on Convolutional Neural Network 计算机科学, 2019, 46(5): 279-285. https://doi.org/10.11896/j.issn.1002-137X.2019.05.043 |
| [8] | 陈俊, 郑洪源. 一种基于FAsT-Match算法的多靶位定位方法 Multi-target Localization Method Based on FAsT-Match Algorithm 计算机科学, 2018, 45(9): 283-287. https://doi.org/10.11896／j.issn.1002-137X.2018.09.047 |
| [9] | 袁佳欣, 陈建新, 肖俊, 吴道亮. 基于回填算法的时间感知的最小区域任务调度算法 Time-aware Minimum Area Task Scheduling Algorithm Based on Backfilling Algorithm 计算机科学, 2018, 45(8): 100-104. https://doi.org/10.11896/j.issn.1002-137X.2018.08.018 |
| [10] | 刘壮,柴秀娟,陈熙霖. 双通道Faster R-CNN在RGB-D手部检测中的应用 Application of Two-stream Faster R-CNN in RGB-D Hand Detection 计算机科学, 2018, 45(5): 232-237. https://doi.org/10.11896/j.issn.1002-137X.2018.05.040 |
| [11] | 刘文龙, 张晶, 周绥平, 李月龙. 基于Repast Simphony平台的人群运动行为仿真及优化 Simulation and Optimization of Crowd Movement Behavior Based on Repast Simphony Platform 计算机科学, 2018, 45(12): 187-191. https://doi.org/10.11896／j.issn.1002-137X.2018.12.030 |
| [12] | 李东民,李静,林华锋. 基于故障树分析的嵌入式系统AADL模型可靠性分析方法 Reliability Analysis Method of Embedded System AADL Model Based on Fault Tree Analysis 计算机科学, 2017, 44(6): 182-188. https://doi.org/10.11896/j.issn.1002-137X.2017.06.031 |
| [13] | 侯金奎,王磊. 基于体系结构的模型转换语义描述框架 Formal Framework of Architecture-based Model Transformation 计算机科学, 2017, 44(4): 148-152. https://doi.org/10.11896/j.issn.1002-137X.2017.04.032 |
| [14] | 贾建鑫,刘广钟,徐明. DTN中基于时空和社会性的概率路由算法 Probability Routing Algorithm in DTN Based on Time and Space and Sociality 计算机科学, 2016, 43(Z6): 295-300. https://doi.org/10.11896/j.issn.1002-137X.2016.6A.071 |
| [15] | 周娟. 基于Ray-Casting算法对医学图像进行三维体绘制重建 3D-volume Reconstruction of Medical Images Based on Ray-Casting Algorithm 计算机科学, 2016, 43(Z11): 156-160. https://doi.org/10.11896/j.issn.1002-137X.2016.11A.034 |
|
||
首页