Simulating and Analyzing Railway Interlockings in ExSpect

This paper describes a study on simulating and analyzing interlocking specifications in the Interlocking Specification Language (ISL), using the tool ExSpect. ExSpect is a toolkit based on the theory of coloured Petri nets.

An approach to translating ISL to ExSpect is suggested. Experimental results of simulating and analyzing part of an ISL specification in ExSpect are discussed. ExSpect seems to be useful for simulating and analyzing ISL specifications. Furthermore, several interesting topics for future research are identified.

(postscript / pdf version of the complete paper)

Back to the list of Technical Reports.