Visualizing formal models

Models are written in a domain specific language (the Axini Modeling Language) using a text editor included in our web application. The models can be visualized to inspect the states and transitions of the underlying symbolic transition system. When a user clicks on a state or transition in the visualization, the interface navigates to the corresponding location in the textual model. This aids modelers in understanding and reasoning about their models.

Even a small conceptual model with a concise visualization quickly becomes hard to comprehend due to overlapping edges and labels. Models of real systems are generally quite large and complex. Different visualization techniques (or combinations thereof) are desired for improved reasoning about such models.

Additionally, certain concepts in the modeling language, such as parallelism, synchronization, non-determinism and time, cannot (yet) be visualized effectively.

Linking the visualization to the model text is sometimes difficult when models make use of macros, where the actual definition of a part of a model is hidden inside a macro. The tool currently jumps inside the macro, but users often want to see where the macro is used. A research direction is how to deal with source code locations for generated code and meta-programming in general.

Another visualization topic is visualizing coverage and test execution. Users can see test case coverage and final states, but not how the system 'walked through' the model during test execution. A temporal visualization with video player-like controls could allow users to animate or step through the execution path.