The Formalized Modeling And Model Analyzing Of The Interlocking Software Based On Interval Timed Colored Petri Nets

In the fields of the computer application, the interlocking system of the railway station is not only the real-time system, but also the safety-critical system. This system has the same significant feature as space, nucleus and military systems, whether this system is running correctly or not has a significant impact on human's life and property safety or environment. Although the time parameter of this system is very important, running of this system safely is much more critical. So much more importance is being attached to the formalization description of the interlocking system of the railway station while the computer technology and the intelligent controlling technology are fully developed and used today. Most of the existing tools to formally describe the interlocking system of the railway station are the petri nets and extended petri nets technic. The existing technic is mostly limited to the logics correctness and the simplifying of the model. The time-restricted modeling and the analysis of the model have been rarely reported by now.This paper mostly investigates the formalized modeling of the interlocking system of the railway station and the safety analysis of the model. Based on the existing time petri nets model and colored petri nets model, together with the Interval Timed Colored Petri Nets (ITCPN), this paper models the logics of the interlocking system of the railway station and analyzes the model. ITCPN model is more close to the real system (the delay is specified by the upper and lower bound, i.e. an interval).The main real research case in this paper is the interlocking system of the railway station, there are other common application cases as well as. It is demonstrated in this paper that the ITCPN is suitable for describing the safe-critical system and the ITCPN model can be analyzed by using abundant theory and practice cases.