Computer Science ›› 2019, Vol. 46 ›› Issue (6): 180-188.doi: 10.11896/j.issn.1002-137X.2019.06.027

Previous Articles     Next Articles

SCR Requirement Model Transformation Based on Table Expression

LI Si-jie, WEI Ou, ZHAN Yun-jiao, WANG Li-song   

  1. (College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211100,China)
  • Received:2018-05-08 Published:2019-06-24

Abstract: The process of requirement specification based on formal methods is based on strictly defined semantics and mathematical models,making the presentation of requirements clearer and easier to understand.SCR method is a forma-lized requirement specification method based on formal symbol-tabular expression,which uses multi-dimensional tabular structure to represent system requirements.The automated testing and verification tools for formal requirements increase the accuracy of the requirements and the efficiency of analysis.However,some current tools lack of automatic verification of safety properties and can’t guarantee the safety of the requirements.Therefore,this paper expanded T-VEC tool based on SCR method,developed model transform tool T2N with the help of language parser generator antlr,designed anguage structure transformation rules,and transformed requirement description language T-VEC based on SCR method into symbolic model checking language XMV,to achieve automatic verification of the extracted system safety properties.Finally,an example of a typical case lighting control system in requirement engineering was used for experimental analysis to verify the effectiveness of the T2N tool and the safety of the requirement model.

Key words: Antlr tool, Model transform, SCR method, T2N tool

CLC Number: 

  • TP311
[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] QI Jian, HU Jun, GU Qing-fan, RONG Hao, ZHAN Wan-li, DONG Yan-hong. Class Flattening Method for AltaRica 3.0 Model [J]. Computer Science, 2021, 48(5): 51-59.
[2] YU Zhi-yong, LIN Li-qiang, CHEN Yan, ZHOU Tian, NI Yi-tao, CHEN Xing. SQL Access Framework for Hyperledger Fabric [J]. Computer Science, 2021, 48(11): 54-61.
[3] CHEN Shuo, HU Jun, TANG Hong-ying, SHI Meng-ye. Transformation Method for AltaRica3.0 Model to NuSMV Model [J]. Computer Science, 2020, 47(12): 73-86.
[4] ZHAN Yun-jiao, WEI Ou and HU Jun. Formal Description of Requirement of Slats and Flaps Control System for DO-178C Case [J]. Computer Science, 2018, 45(4): 196-202.
[5] LI Dong-min, LI Jing and LIN Hua-feng. Reliability Analysis Method of Embedded System AADL Model Based on Fault Tree Analysis [J]. Computer Science, 2017, 44(6): 182-188.
[6] HOU Jin-kui and WANG Lei. Formal Framework of Architecture-based Model Transformation [J]. Computer Science, 2017, 44(4): 148-152.
[7] GUO Peng, LI Ya-hui, SUN Lei and CAI Xiao-le. UML Model to Simulink Model Transformation Method in Design of Embedded Software [J]. Computer Science, 2016, 43(2): 192-198.
[8] HU Xiang, JIAO Li and CHAI Ye-sheng. Transforming UML to GSPN for Performance Analysis [J]. Computer Science, 2016, 43(11): 49-54.
[9] LI Zong-hua, ZHOU Xiao-feng, WU Ke-li and CHEN Fu-bing. BPMN Formalization Based on Extended Petri Nets Model [J]. Computer Science, 2016, 43(11): 40-48.
[10] SU Yue, LI Mi, WANG Wen-xin and ZHANG De-ping. Software Reliability Prediction Approach Based on UML Activity Diagram [J]. Computer Science, 2015, 42(Z6): 531-536.
[11] MA Li, WU Guo-qing, HUANG Bo, CHENG Ming and CUI Meng-tian. Visualization Method of BDL Model to UML State Diagram [J]. Computer Science, 2015, 42(7): 38-43.
[12] SUN Lei, YANG Hai-yan and WU Ji. Simulation and Real-time Analysis for Embedded Software Design Model with Consideration of Integrated Modular Avionics Platform [J]. Computer Science, 2015, 42(12): 95-97.
[13] WANG Shi-qi, LI Yi-xiao, SHEN Li-wei and ZHAO Wen-yun. Display Process and Technique Implementation of Ontology Conceptual Diagram [J]. Computer Science, 2015, 42(12): 87-91.
[14] HUANG Xiang and CHEN Zhi-gang. Performance Modeling Approach for Resource Sensitive Distributed Systems [J]. Computer Science, 2013, 40(9): 174-181.
[15] LI Zhen-song GU Bin. Research on Verification Method of AADI. Behavior Model Based on I1ppaal [J]. Computer Science, 2012, 39(2): 162-169.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!