Model-based variable and transition orderings for efficient symbolic model checking

The symbolic model checker NuSMV has been used to check safety properties for railway interlockings. When the size of the models increased, the model checking efficiency decreased dramatically to a point at which the verification failed due to lack of memory. At that point the models we could check were still small in the real world of railway interlockings. Various standard options to the NuSMV model checker were tried, mostly without significant improvement. However, the analysis of our model provided information on how to optimise the variable orderings and also the ordering and clustering of the partitioned transition relation. The NuSMV code was adapted to enable user control for ordering and clustering of transitions. This replacement of the tool's generic algorithm improved efficiency enormously, enabling the checking of safety properties for very large models. This paper discusses how the characteristics of our model are used to find the optimised parameters.