Author(s)

W. Tang, B. Ning, T. Xu & L. Zhao

Abstract

The high quality System Requirement Specification (SRS) is at the heart of the design and development of the European Train Control System level 2 (ETCS L2) with high safety and efficiency. However, the SRS, written in natural language with a shortage of rigorous mathematic foundation, makes it difficult to meet the high quality attributes of SRS, such as correctness, completeness and consistency. In order to tackle the above problems, the integration of a scenariobased model with a formal method, which is recommended to model and verify safety critical system (e.g., train control system), is proposed to improve the quality of the SRS for ETCS L2. First, the relevant operational scenarios are extracted from the SRS, then the corresponding UML sequence diagrams are constructed and finally the sequence diagrams are verified by the formal analysis tool (i.e., NuSMV) through a series transformation rules from UML sequences to NuSMV. The output analysis results facilitate improvement of the SRS qualities. Within the above modeling and verification process, the key mapping relationship is presented to ensure the consistency and traceability between the UML sequence model and the NuSMV specification. Keywords: European train control system, modeling and verification, scenario, sequence diagram, model checking. 1 Introduction The European Train Control System (ETCS) is a signaling, control and train protection system currently used by European railways. The ETCS can be configured to operate in a certain level. In this paper we take level 2 (ETCS L2)

Keywords

European train control system, modeling and verification, scenario,sequence diagram, model checking