计算机科学 ›› 2019, Vol. 46 ›› Issue (6): 180-188.doi: 10.11896/j.issn.1002-137X.2019.06.027
李思洁, 魏欧, 战芸娇, 王立松
LI Si-jie, WEI Ou, ZHAN Yun-jiao, WANG Li-song
摘要： 基于形式化方法的需求规约过程以严格定义的语义和数学模型为基础,使得需求的表述更加清晰明了,易于理解。SCR方法是一种基于形式化符号-表格的表达式,以多维表格化结构表示系统需求的形式化需求规约方法。针对形式化需求的自动化测试和检验工具提高了需求分析的正确性和效率性,但目前工具缺少安全性质的自动验证,无法保证需求的安全性。因此,文中对基于SCR方法的T-VEC工具进行扩展,在语言解析器生成器antlr(ANother Tool for Language Recognition)的辅助下开发了模型转换工具T2N,设计了语言结构转换规则,将基于SCR的需求描述语言T-VEC转换为符号化模型检测语言XMV,以实现对提取的系统安全性质的自动化验证。最后,以需求工程中的典型案例——灯光控制系统为例进行实验分析,验证T2N工具的有效性和需求模型的安全性。
中图分类号:
| [1]HEITMEYER C,BHARADWAJ R.Applying the SCR Requirements Method to the Light Control Case Study[J].Journal of Universal Computer Science,2000,6(7):88-92. [2]THAYER R,DORFMAN M.Software Requirements Analysis and Specifications [M].Wiley-IEEE Press,2000. [3]GOODRUM M,CLELAND-HUANG J,et al.What Require-ments Knowledge Do Developers Need to Manage Change in Safety-Critical Systems?[C]∥Requirements Engineering Conference.IEEE,2017:90-99. [4]JIN Y,PARNAS D L.Defining the meaning of tabular mathematical expressions[J].Science of Computer Programming,2010,75(11):980-1000. [5]HEITMEYER C L,LEONARD E I.Obtaining trust in autonomous systems:tools for formal model synthesis and validation[C]∥2015 IEEE/ACM 3rd FME Workshop on Formal Me-thods in Software Engineering (FormaliSE).IEEE,2015:54-60. [6]MARCINIAK,JOHN J.Encyclopedia of Software Engineering [M]∥Encyclopedia of Software Engineering,1994. [7]HEITMEYER C L,JEFFORDS R D.Applying a Formal Re-quirements Method to Three NASA Systems:Lessons Learned[C]∥Aerospace Conference.2007:1-10. [8]HU J,SHI J J,CHENG H,et al.A four-variable model based system security modeling and analysis method[J].Computer Science,2016,43(11):193-199.(in Chinese) 胡军,石娇洁,程桢,等.一种基于四变量模型的系统安全性建模与分析方法[J].计算机科学,2016,43(11):193-199. [9]PARNAS D L,MADEY J.Functional Documentation for Computer Systems Engineering (Version 2) [J].CRL Report,1991,7(237). [10]BLACKBURN M R,BUSSER R D.T-VEC:a tool for developing critical systems[C]∥Proceedings of 11th Annual Confe-rence on Computer Assurance.1996:237-249. [11]CHANDLER R E.Model Checking[M]∥Encyclopedia of Biostatistics 2005. [12]BULTAN T,HEITMEYER C.Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems[J].Design Automation for Embedded Systems,2008,12(1-2):97-137. [13]KRÖGER F.Temporal Logic of Programs[C]∥Etacs Monographs on Theoretical Computer Science.1987. [14]CAVADA R,CIMATTI A,DORIGATTI M.The nuXmv Symbolic Model Checker[C]∥International Conference on Compu-ter Aided Verification.2014,pp:334-342. [15]CIMATTI A,CLARKE E,GIUNCHIGLIA F.NUSMV:a new symbolic model checker[J].International Journal on Software Tools for Technology Transfer,2000,2(4):410-425. [16]BIERNACKA A,BIERNACKI J,SZPYRKA M.State-based verification of RTCP-nets with nuXmv[C]∥AIP Conference Proceedings.2015:375-390. [17]CHOI Y,HEIMDAHL M P E.Model Checking RSML-e Requirements[C]∥IEEE International Symposium on High Assurance Systems Engineering.2002:109. |
| [1] | 祁健, 胡军, 谷青范, 荣灏, 展万里, 董彦宏. 一种AltaRica 3.0模型中类的平展化方法 Class Flattening Method for AltaRica 3.0 Model 计算机科学, 2021, 48(5): 51-59. https://doi.org/10.11896/jsjkx.200700184 |
| [2] | 於志勇, 林力强, 陈艳, 周天, 倪一涛, 陈星. 面向Hyperledger Fabric的SQL访问框架 SQL Access Framework for Hyperledger Fabric 计算机科学, 2021, 48(11): 54-61. https://doi.org/10.11896/jsjkx.210100220 |
| [3] | 陈朔, 胡军, 唐红英, 石梦烨. 一种AltaRica3.0模型到NuSMV模型的转换方法 Transformation Method for AltaRica3.0 Model to NuSMV Model 计算机科学, 2020, 47(12): 73-86. https://doi.org/10.11896/jsjkx.190400035 |
| [4] | 战芸娇,魏欧,胡军. 面向DO-178C的襟缝翼控制系统需求的形式化描述 Formal Description of Requirement of Slats and Flaps Control System for DO-178C Case 计算机科学, 2018, 45(4): 196-202. https://doi.org/10.11896/j.issn.1002-137X.2018.04.033 |
| [5] | 李东民,李静,林华锋. 基于故障树分析的嵌入式系统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 |
| [6] | 侯金奎,王磊. 基于体系结构的模型转换语义描述框架 Formal Framework of Architecture-based Model Transformation 计算机科学, 2017, 44(4): 148-152. https://doi.org/10.11896/j.issn.1002-137X.2017.04.032 |
| [7] | 郭鹏,李亚晖,孙磊,蔡晓乐. 面向嵌入式软件开发的UML到Simulink模型转换方法 UML Model to Simulink Model Transformation Method in Design of Embedded Software 计算机科学, 2016, 43(2): 192-198. https://doi.org/10.11896/j.issn.1002-137X.2016.02.042 |
| [8] | 胡翔,焦莉,柴叶生. 从UML到GSPN的转换和性能分析方法 Transforming UML to GSPN for Performance Analysis 计算机科学, 2016, 43(11): 49-54. https://doi.org/10.11896/j.issn.1002-137X.2016.11.009 |
| [9] | 李宗花,周晓峰,吴克力,陈伏兵. 基于扩展Petri网模型的BPMN形式化 BPMN Formalization Based on Extended Petri Nets Model 计算机科学, 2016, 43(11): 40-48. https://doi.org/10.11896/j.issn.1002-137X.2016.11.008 |
| [10] | 马 丽,毋国庆,黄 勃,程 铭,崔梦天. BDL模型到UML状态图的可视化方法研究 Visualization Method of BDL Model to UML State Diagram 计算机科学, 2015, 42(7): 38-43. https://doi.org/10.11896/j.issn.1002-137X.2015.07.009 |
| [11] | 孙磊,杨海燕,吴际. 基于IMA平台的嵌入式软件设计模型仿真及实时性分析方法 Simulation and Real-time Analysis for Embedded Software Design Model with Consideration of Integrated Modular Avionics Platform 计算机科学, 2015, 42(12): 95-97. |
| [12] | 王诗碕,李伊潇,沈立炜,赵文耘. 本体概念图的展示过程及技术实现 Display Process and Technique Implementation of Ontology Conceptual Diagram 计算机科学, 2015, 42(12): 87-91. |
| [13] | 黄翔,陈志刚. 资源敏感的分布式系统性能建模方法 Performance Modeling Approach for Resource Sensitive Distributed Systems 计算机科学, 2013, 40(9): 174-181. |
| [14] | 朱梅霞，武继刚. MARTE顺序图到TTS4SD的转换 Approach to Transforming MARTS Sequence Diagram to TTS4SD Models 计算机科学, 2013, 40(1): 175-178. |
| [15] | 黄镇谨，陆阳，杨娟，方欢. 混合Petri网的流体随机Petri网模型 Fluid Stochastic Petri Net Model for Hybrid Petri Net 计算机科学, 2012, 39(8): 51-54. |
|
||
首页