The Formal Verification For The Security Of Trackside System

The trackside system is one of the sub-systems with the highest level of security in the train control system.If a problem arises,the losses may be caused for the personal and property safety of train passengers so that it will lead to the irreparable consequences.Therefore,it is an urgent problem that how to guarantee the security of trackside system.The model checking in the formal verification method can achieve the verification objective by traversing the system spaces in order to guarantee the system in accordance with the corresponding security demands.However,since the physical environment and system behavior of trackside system are very complicated,it occurs that the state space of the system exceeds the limitation of the verification tool with the model checking method gradually applied to the trackside system,thus leading to verification failure.With the further development of verification work,it is founded that there are two basic situations in the trackside system verification process: firstly,some security demands are only related to parts of input variables,thus the projection method can be utilized to control the complexity of system.Secondly,some variables have causal relationship.Therefore,the causal relationship among the variables shall be analyzed in order to try to find the method of reducing system complexity.A state-space reduction method based on the projection and causal relationship is proposed in this paper.Firstly,the problem diagram was used for the description of trackside system,and the relationship between trackside system and its verification system was then analyzed so as to gain the problem graph of trackside verification system.Later,the security sub-property was chosen as the projection dimension to define the projection operator and to project the original trackside verification system based on this.By these above,the smaller verification module,operational environment and security demand will be acquired.The paper also analyzed all kinds of causal relationship among the variables inside the device and proposed the reduction method for the variables according to the causal relationship so as to reduce the variable number actually used in the verification process and further decrease the state spaces generated in the verification.Finally,data collected from practical project is combined to show the complete reduction and verification process of trackside system.With the iZC in the iCMTC System as the system to be verificated,data actually generated in a subway line was collected as the environment to verify the iZC system.The experimental results show that the method proposed in the paper could reduce the state of verification system effectively,decrease the state spaces in the model verification and promote the verification efficiency of model checking method in the trackside system significantly.At last,the verification for the security of trackside system was completed successfully.