A track plan 1 is rendered as an attributed graph (Fig.2) whose nodes represent the geographical position of individual assets (e.g. balises 14, 15). A set of rules correspond to their correct geographical positions. A set of axioms in first order logic define the behaviour of the graph and annotations thereon. For an individual railway asset, a bounded search of the graph using a pre-determined set of bounds is executed 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 (Fig.4). The rule check may be carried out by an automatic theorem prover as an SMT (Satisfiability Modula Theories) problem simulating a breadth-first search. The maximum value of the variable bound ‘k’ and individual railway asset may be selected by a user or the search may be executed for each asset.
Railway signalling design checker
2024-03-27
Patent
Electronic Resource
English
Model checker for railway signalling communication protocol
British Library Conference Proceedings | 2006
|Engineering Index Backfile | 1909
|