A Method of Generating Engineering Test Sequence for Urban Rail Transit CBTC System Based on Formalization. Issue 1 (June 2020)