Grounded Language Design for Lightweight Diagramming for Formal Methods

TL;DR

This paper introduces a domain-specific language for lightweight, effective diagramming in formal methods tools, grounded in cognitive science and validated through evaluation, to improve model visualization without extensive effort.

Contribution

It designs a new diagramming language based on cognitive principles and key domain elements, integrated into an Alloy-like tool for better model visualization.

Findings

Diagrams are effective for reasoning about models.

The language is lightweight and easier to use than full visualizations.

It fills a niche for domain-driven, cognitively sound diagramming tools.

Abstract

Model finding, as embodied by SAT solvers and similar tools, is used widely, both in embedding settings and as a tool in its own right. For instance, tools like Alloy target SAT to enable users to incrementally define, explore, verify, and diagnose sophisticated specifications for a large number of complex systems. These tools critically include a visualizer that lets users graphically explore these generated models. As we show, however, default visualizers, which know nothing about the domain, are unhelpful and even actively violate presentational and cognitive principles. At the other extreme, full-blown visualizations require significant effort as well as knowledge a specifier might not possess; they can also exhibit bad failure modes (including silent failure). Instead, we need a language to capture essential domain information for lightweight diagramming. We ground our language design in both the cognitive science literature on diagrams and on a large number of example custom visualizations. This identifies the key elements of lightweight diagrams. We distill these into a small set of orthogonal primitives. We extend an Alloy-like tool to support these primitives. We evaluate the effectiveness of the produced diagrams, finding them good for reasoning. We then compare this against many other drawing languages and tools to show that this work defines a new niche that is lightweight, effective, and driven by sound principles.