Application of coloured petri nets in modelling and simulating a railway signalling system

Abstract

Formal validation of railway signalling systems normally involves three processes: creating models; simulation; and verifying the models’ dynamic behavior against the specified properties. It is wellknown that the third process often encounters the problem of state explosion. To achieve fully automated formal validation, researchers usually abstract away details of operating procedures and concentrate on route interlocking that prevents train collision and derailment. Thus we encounter a dilemma between fully automated validation of an incomplete model or partial, semi-automated validation of a complete model. We argue that formally modelling the complete model will be more valuable for the on-going projects of the State Railway of Thailand because they provide insights and can be used to train new signal engineers. This paper focuses on the complete Coloured Petri Net (CPN) model of a typical Thai railway signalling system: a double-line station with one passing loop. The CPN model has included train movements that can be simulated and graphically visualized. In particular we illustrate how the CPN diagrams capture nine properties: Route interlocking, Flank protection, Approach signal release, Aspect sequence, Approach lock, Back lock, Alternative overlap, Sectional route release and Quick route release. Lessons learnt from using CPN Tools to model and validate the railway signalling systems are also discussed.