轨道交通控制软件中基于场景的需求分析方法

doi:10.19678/j.issn.1000-3428.0058548

摘要/Abstract

摘要： 针对轨道交通控制软件的形式化方法，在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程，为形式化规约构建提供模板。在对需求的确认和验证中，根据形式化规范建立需求模型，导出相关图表，基于此检查领域专家关注的场景。同时制定场景描述规则，使场景可以在需求模型中正确执行。在此基础上，从特殊变量、效率、场景质量三方面对场景进行优化，更充分地验证需求的正确性。实验结果表明，对于典型车载控制软件，该方法较传统分析方法可多探测到10%的潜在缺陷，效率提升80%以上。

关键词: 形式化方法, 需求规约, 需求确认和验证, 场景优化, 轨道交通控制软件

Abstract: In practical engineering applications, the existing formal methods for railway control software are limited by the difficulties in formal modeling and verification in system-level scenarios. To address the problem, a formal modeling and requirement validation method for rail transit is proposed. The method adopts a three-step template for requirement formalization, turning the informal requirements into semi-formal ones, and then into formal requirement specifications. During the confirmation and verification of requirements, the formal specification is used to establish the requirement model, and then the related charts are derived. On this basis, the scenarios concerned by domain experts are checked. At the same time, the rules of scenario description are formed to make the scenario executed correctly in the requirement model. Then the scene is optimized from three aspects of special variables, including the special variables, efficiency and scene quality, so as to verify the correctness of the requirements more fully. The experimental results show that compared with the traditional analysis method, this method can detect 10% more potential defects and improve the efficiency by more than 80% for typical onboard control software.

Key words: formal method, requirement specification, requirement validation and verification, scenario optimization, railway control software

中图分类号:

TP311.521

闫倩倩, 缪炜恺. 轨道交通控制软件中基于场景的需求分析方法[J]. 计算机工程, 2021, 47(8): 284-293,300.

YAN Qianqian, MIAO Weikai. Scenario-based Requirement Analysis Method for Railway Control Software[J]. Computer Engineering, 2021, 47(8): 284-293,300.

https://www.ecice06.com/CN/Y2021/V47/I8/284

图/表 14

20210819202501

20210819202504

20210819202508

20210819202513

20210819202519

20210819202525

20210819202529

20210819202533

20210819202538

20210819202543

20210819202547

20210819202552

20210819202556

20210819202600

参考文献

[1] HALL A.Realising the benefits of formal methods[C]//Proceedings of the 7th International Conference on Formal Methods and Software Engineering.New York, USA:ACM Press, 2005:1-4.
[2] 陈铭松, 鲍勇翔, 孙海英, 等. 基于通信的列车控制系统可信构造:形式化方法综述[J]. 软件学报, 2017, 28(5): 1183-1203. CHEN M S, BAO Y X, SUN H Y, et al. Survey on formal method of trustworthy construction for communication-based train control systems[J]. Journal of Software, 2017, 28(5): 1183-1203.(in Chinese)
[3] 王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2019, 30(1): 33-61. WANG J, ZHAN N J, FENG X Y, et al. Overview of formal methods[J]. Journal of Software, 2019, 30(1): 33-61.(in Chinese)
[4] LIU S Y.Formal engineering for industrial software development:using the SOFL method[M]. Beijing:Tsinghua University Press, 2013.
[5] 胡雪莲.基于UML和UPPAAL的CTCS-3级列控系统等级转换场景建模与验证[D]. 兰州:兰州交通大学, 2015. HU X L.Modeling and verification of level transition scene in CTCS-3 level train control system based on UML and UPPAAL[D]. Lanzhou:Lanzhou Jiaotong University, 2015.(in Chinese)
[6] BLOEM R, CIMATTI A, GREIMEL K, et al. RATSY-a new requirements analysis tool with synthesis[C]//Proceedings of International Conference on Computer Aided Verification.Berlin, Germany:Springer, 2010:425-429.
[7] YUAN L, TANG T, LI K C.Modelling and verification of the system requirement specification of train control system using SDL[C]//Proceedings of International Symposium on Autonomous Decentralized Systems.Berlin, Germany:Springer, 2011:81-85.
[8] MILNER R.A calculus of communicating systems[M]. Berlin, Germany:Springer, 1980.
[9] HOAREE C A R.Communicating sequential processes[M]. Englewood Cliffs, USA:Prentice Hall, 1985.
[10] 陈金鑫, 苏雯.基于Event-B的自动化模块组合方法研究[J]. 计算机工程, 2019, 45(5): 298-307, 314. CHEN J X, SU W.Research on automated module composition method based on Event-B[J]. Computer Engineering, 2019, 45(5): 298-307, 314.(in Chinese)
[11] JACKY J.The way of Z:practical programming with formal methods[M]. Cambridge, UK:Cambridge University Press, 1997.
[12] JEAN-RAYMOND A.Modeling in Event-B-system and software engineering[M]. Cambridge, UK:Cambridge University Press, 2013.
[13] DANIEL A, HYUNSOOK D, SEOK-WON L.SQ^(2)E:an approach to requirements validation with scenario question[C]//Proceedings of the 17th Asia Pacific Software Engineering Conference.Sydney, Australia:[s.n.], 2010:1-10.
[14] YOUN K L, HOH P I, RICK K.Customer requirements validation method based on mental models[C]//Proceedings of the 21st Asia Pacific Software Engineering Conference.Jeju, South Korea:[s.n.], 2014:199-206.
[15] DANIEL A, HYUNSOOK D, SEOK-WON L.Interactive requirements validation for reactive systems through virtual requirements prototype[C]//Proceedings of 2011 Model-Driven Requirements Engineering Workshop.Washington D.C., USA:IEEE Press, 2011:1-5.
[16] JOHN S F, PETER G L, SHIN S.VDMTools:advances in support for formal modeling in VDM[J]. ACM SIGPLAN Notices, 2008, 43(2): 3-11.
[17] MICHAEL L, MICHAEL B.ProB:a model checker for B[C]//Proceedings of International Symposium of Formal Methods Europe.Berlin, Germany:Springer, 2003:855-874.
[18] MIAO W K, PU G G, YAO Y B, et al. Automated requirements validation for ATP software via specification review and testing[C]//Proceedings of International Conference on Formal Engineering Methods.Berlin, Germany:Springer, 2016:26-40.
[19] 赵梦瑶, 陈小红, 孙海英, 等. 轨道交通联锁领域特定语言的形式化[J]. 软件学报, 2020, 31(6): 1638-1653. ZHAO M Y, CHEN X H, SUN H Y, et al. Formalizing railway interlocking domain specific language[J]. Journal of Software, 2020, 31(6): 1638-1653.(in Chinese)
[20] RALUCA M, HENRIK K, MARIUS M, et al. Analyzing industrial architectural models by simulation and model-checking[C]//Proceedings of International Workshop on Formal Techniques for Safety-Critical Systems.Berlin, Germany:Springer, 2014:189-205.
[21] EMMANOUELA S, ANASTASIA M, PANAGIOTIS K, et al. Early validation of system requirements and design through correctness-byconstruction[J]. Journal of Systems and Software, 2018, 145:52-78.
[22] PRZEMYSLAW D, THOMAS A H, JAN K, et al. Faster statistical model checking for unbounded temporal properties[J]. ACM Transactions on Computational Logic, 2017, 18(2): 1-25.
[23] DAVID H.Statecharts:a visual formalism for complex systems[J]. Science of Computer Programming, 1987, 8(3): 231-274.
[24] The MathWorks, Inc.The MathWorks:stateflow and stateflow coder, users guide[EB/OL]. [2020-06-10]. http://www.mathworks.com/help/releases/R13sp2/pdfdoc/stateflow/sfug.pdf.
[25] MELISSA I, LEILA K, ANTOINE R. Scenario-oriented reverse engineering of complex railway system specifications[J]. Systems Engineering, 2018, 2:91-104.
[26] JAE E S, ALISTAIR G S, ANDREAS G. Scenario advisor tool for requirements engineering[J]. Requirements Engineering, 2005, 2:132-145.
[27] OLIVEIRA K, OLIVEIRA V, JULIA S. Using linear logic to verify requirement scenarios in SOA models based on inter organizational work flow nets relaxed sound[C]//Proceedings of the 19th International Conference on Enterprise Information Systems. Washington D. C., USA:IEEE Press, 2017:254-262.
[28] 杨广华, 齐璇, 施寅生. 基于场景模式的嵌入式软件测试用例设计[J]. 计算机工程, 2010, 36(15): 89-91. YANG A H, JI X, SHI Y S. Design of embedded software test cases based on scenario pattern[J]. Computer Engineering, 2010, 36(15): 89-91.(in Chinese)
[29] 吕照进, 沈立炜, 赵文耘. 面向场景的安卓应用代码定位方法[J]. 计算机科学, 2017, 44(2): 216-221, 256. LÜ Z J, SHEN L W, ZHAO W Y. Scenario-oriented location method of android applications[J]. Computer Science, 2017, 44(2): 216-221, 256.(in Chinese)

选择文件类型/文献管理软件名称

选择包含的内容