A computer-implemented method of checking the design of a railway signalling scheme is described. A track plan is rendered as an attributed graph, with a set of rules and axioms in first order logic defining the behaviour of the graph, along with annotations on the graph, used to determine whether or not the geographical position of an individual railway asset on the track plan is correct. Each rule corresponds to the correct geographical position of an individual railway asset. For each individual railway asset, a bounded search of the annotated graph using a pre-determined set of bounds to check whether a rule corresponding to the correct geographical position of the individual railway asset holds true. The pre-determined set of bounds contains a variable bound k that is incrementally increased until the result of the rule check is known.
Railway signalling design checker
2022-11-09
Patent
Electronic Resource
English
Model checker for railway signalling communication protocol
British Library Conference Proceedings | 2006
|