| Towards the Mechanical Verification of Moving Block Signalling Systems (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. Previous work carried out by the author (and many others) has involved the application of formal descriptions techniques to verifying the correctness of fixed block railway signalling systems. These systems are referred to as such because the railway is divided into sections of track, which are separated by signals. However, in the future, it will become increasingly the case that interlockings will not involve signals at all: safe distances will be kept between trains to avoid collisions (indicated to on-board systems via communication devices), but the railways of the future will not be separated into explicit sections of track as they are now. In this paper we investigate whether model checking techniques, which have previously been applied to fixed block systems, are also applicable to such moving block systems. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||