Grounded Language Design for Lightweight Diagramming for Formal Methods

要約

SAT ソルバーや同様のツールによって具体化されるモデル検索は、埋め込み設定とそれ自体のツールの両方で広く使用されています。
たとえば、Alloy のようなツールは SAT をターゲットにしており、ユーザーが多数の複雑なシステムの高度な仕様を段階的に定義、調査、検証、診断できるようにします。
これらのツールには、ユーザーがこれらの生成されたモデルをグラフィカルに探索できるようにするビジュアライザーが重要に含まれています。
ただし、ここで示したように、ドメインについて何も知らないデフォルトのビジュアライザーは役に立たず、表示原理や認知原理に積極的に違反することさえあります。
逆に、本格的なビジュアライゼーションには多大な労力と、指定子が持っていない可能性のある知識が必要です。
また、不良な障害モード (サイレント障害を含む) を示すこともあります。
代わりに、軽量の図作成のために重要なドメイン情報を取得する言語が必要です。
私たちの言語設計は、図に関する認知科学文献と多数のカスタム ビジュアライゼーションの例の両方に基づいています。
これにより、軽量ダイアグラムの主要な要素が特定されます。
これらを小さな直交プリミティブのセットに抽出します。
これらのプリミティブをサポートするために、Alloy のようなツールを拡張します。
作成された図の有効性を評価し、推論に適していると判断します。
次に、これを他の多くの描画言語やツールと比較して、この作品が軽量で効果的で、健全な原則に基づいた新しい分野を定義していることを示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google