Scenario-based Requirement Analysis Method for Railway Control Software

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.