Modeling and verification of train safety comprehensive monitoring system using temporal Petri nets

Petri nets and temporal logic are efficient tools to study concurrent systems, but each has their own shortages. Thus, we introduce temporal Petri nets to model, analyze and verify train safety comprehensive monitoring system. On one hand, we describe frameworks of this system using Petri nets. On the other hand, we use temporal logic to describe temporal relationships of system states. Then, we analyze and verify the properties of model and conclude that the system is reliable and effective.