Modeling And Verification Of Train Control System Based On STeC

The rapid development of these technology, embedded, computer and network, has greatly improved the life of human beings. Under the guidance of this kind of demand, the Cyber Physical Systems arises at the historic moment, and has aroused great attention from the academic circles and the business circles of the world. The typical applications of CPS include intelligent transportation field,bio medical field, autonomic computing and so on. the application of it requires very high security, thus ensuring the time-space consistency of the agent is a very important work in CPS research. According to the time and space consistency requirements of it, the real-time system specification language STeC is used to model the CPS system, which can verify the correctness in the requirement design of the system.In this paper, the following aspects are included in the main research contents:1, According to the problem of the train delay in intelligent transportation field, For the two different types of two train's delay we design different nonstop overtaking strategy, by substituting actual train's instance data test practica of this method;2, Using STeC in formal specfication of CPS modeling, specially to verify the logic and the time-space considtency of that discription;3, For different instances, using the conversion from STeC to Stateflow migration system, and then using Matlab to model and simulink these two strategies, we can verify the security of the system, and by using static simulation can satisfy the practical application of industry.4, Finally, we design the TrainPassIDE tool to overtake the visual effect more intuitive. this tool can get the user's input of the different parameters of the trains,then we can observe the different results of these two different types of train delay.