State space analysis of a railway network
Jonathan Billington, Chris Janczura · 2002
A railway network consisting of a single track with a passing loop and a number of trains moving in the same direction is modelled by a coloured Petri net (CPN), and then analyzed using the software tools Design/CPN/sup TM/ and Occurrence Graph Analyzer OGA/sup TM/. Certain safety and operational properties 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.