作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2021, Vol. 47 ›› Issue (8): 284-293,300. doi: 10.19678/j.issn.1000-3428.0058548

• 开发研究与工程应用 • 上一篇    下一篇

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

闫倩倩, 缪炜恺   

  1. 华东师范大学 上海市高可信计算重点实验室, 上海 200062
  • 收稿日期:2020-06-04 修回日期:2020-07-15 发布日期:2020-07-22
  • 作者简介:闫倩倩(1995-),女,硕士研究生,主研方向为软件需求与建模、软件测试;缪炜恺,副教授。
  • 基金资助:
    国家自然科学基金面上项目“数据驱动的机器学习软件系统的形式化需求建模工程方法”(61872144);国家自然科学基金青年基金“嵌入式控制软件的形式化规格说明构建的工程方法”(61402178)。

Scenario-based Requirement Analysis Method for Railway Control Software

YAN Qianqian, MIAO Weikai   

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China
  • Received:2020-06-04 Revised:2020-07-15 Published:2020-07-22

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

中图分类号: