Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL

Abstract

This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified.