Abstract:
The Regional Data Center (RDC), as the core trackside equipment of CTCS-1 train control system, provides track data, temporary speed restriction, and route information to the on-board equipment. Therefore, the correctness of RDC data is crucial to train operation safety. In this paper, the static data stored in RDC were analyzed and the constraints for them were summarized. Taking the track section data as an example, the data constraint rules were established based on the domain value conditions for entity data and the relationship between the data, the data validation rules were added into the data validation process which was modelled by using the communication sequence process (CSP) formal language. Finally, the model checker ProB was used to check the correctness of the CSP semantic models. The validation results are correct, which shows that the data validation method is feasible and lays a foundation for the automatic verification of RDC static data.