Scenario-based modeling and verification for CTCS-3 system requirement specification

The Chinese train control system level 3 (CTCS-3) system requirement specification required to be high-quality should satisfy the quality attributes, such as correctness, completeness, consistency, and traceability. In order to prove that these quality attributes are satisfied, we present a scenario-based approach using UML sequence diagram and model checking to modeling and verify the specification. The mapping between scenario and sequence diagram ensures correctness of the modeling, and enhances the traceability of the verification. The expressiveness of sequence diagram and the precise semantics of model checker are outstanding and proved in practical applications. The formal techniques used in this paper provide a certain level of confidence because of their rigor and completeness.