In: Proceedings 1996 IEEE International Conference on Systems, Man and Cybernetics (SMC'96), Vol. 3, Beijing, China, Oct. 14-17, 1996, pages 2386-2391. IEEE, October 1996.
Abstract: A railway network consisting of a single track with a passing loop and a number of trains moving in the same direction is modelling by a coloured Petri net (CPN), and then analyzed using the software tools Design/CPN and Occurence Graph Analyzer OGA. Certain safety and operational propoerties are formulated and then formally proved by interrogating the complete state space of the system. The notion of strongly connected components is used in some proofs. Analysis of the model revealed some undesirable behaviour including a deadlock.