Visualizations of Formal Specifications

Formal specifications

Visualizations

Formal models (specifications) are powerful tools that provide assurance of system behavior, but whether or not the results are trustworthy hinges upon whether or not the stakeholders understand the behavior of the models and trust the correctness of the underlying specifications. Visualizations provide a way for these stakeholders to gain some insight into the model behavior, but exactly how the visualizations are used is less clear.

In this project, we investigate why and how users of formal models use visualizations to understand model behavior.

We also apply our findings on the design of Penlloy, a new, domain-specific visualizer of the Alloy formal specification language which uses the Penrose diagramming tool as its engine.