Visualisation of large Labelled Transition Systems

A formal model describes the behaviour of a program, protocol or other system. The properties of this model can be verified, such that we can prove these properties with absolute certainty. Visualising the state space of a formal model is an important tool for their development This thesis focuses on visualising such a state space as a graph. We present a layout technique that provides efficient graph layouts for graphs with over 10000 nodes, discuss the effectiveness of different edge shapes, and present multiple ways of highlighting the structure of the graph. We present a rendering procedure capable of rendering graphs larger than 10000 nodes while supporting these techniques. We implemented these techniques in a tool and use it to measure the performance of the techniques. The effectiveness of these techniques is analysed using a survey on the tool in a few practical applications. We conclude that these techniques can effectively be used in one visualisation to assist in formal model development