Modeling The Computer Interlocking System Based On Timed Coloured Petri Nets

With the rapid development of the railway system, the demand for improved the safetyand reliability of the railway system is increasing. Especially a railway computer interlockingsystem, as a safety-critical system, plays a vital role in the achievement of safe and fastoperation. At present, the number of newly built railway is being vigorously built and the oldline was completed to strengthen and reform in our country. In order to be able to assess theperformance of these stations, we need to find the right tools and techniques to determine thequality of these large-scale controls of the railway station. The designer must ensure that areliable system model can be achieved in order to meet the requirements standard ofCENELEC(European Committee for Electrotechnical Standardization). This article is used todevelop the model of the interlocking system on the basis of the existing system model, theaim is to reduce development time and improve system reliability.Petri net is one of the most popular modeling methods currently used, it offers a simpleerror tracking and visualization methods for designers. Petri net is a graphical modelinglanguage and it has been proven to provide a good formal framework for a variety of complexdependencies and a truly concurrent real-time system modeling. Therefore, a high-level Petrinet-Interval time colored Petri net (abbreviation ITCPN) is used to model and analyze thecomputer interlocking system of railway stations in this paper. ITCPN is extended in time ofcolored Petri net, the time of the token and transition determines the delay of each productiontoken. This delay is specified by an upper and lower bounds, that is a time interval. ITCPNallows to model for the dynamic behavior of large and complex systems, such as the modelingand analysis of railway interlocking stations in order to improve the ability to handle the largestation. This article adopts ITCPN to model computer interlocking system for a simplerailway station, so that a computer interlocking system model to meet the SystemRequirements Standard is developed, its composition devices (including signals, switches andtrack circuit) and the process of route setting and locking/unlocking is modeled. Based on this,the formal analysis of each model is completed in order to be able to enrich stationinterlocking system analysis and modeling capabilities.The results show that the ITCPN description method can be used to assess the stationoperation and interlocking device. In the early stages of system development, it‘s verysuitable that the modeling and simulation for interlocking system is used to confirm thefeasibility of the system. In the system development phase, it is also appropriate tool that theformal models are used for formal analysis for the specific attributes, because the model canbe specifically analyzed to verify the specific properties of the model in an abstract way.Therefore, it’s very important that the time colored Petri network is used for interlocking system modeling and formal analysis in the interlocking system design and developmentphase.