CISPA
Browse
cispa_all_3659.pdf (6.39 MB)

Visual Analysis of Hyperproperties for Understanding Model Checking Results

Download (6.39 MB)
Version 2 2023-12-11, 20:14
Version 1 2023-11-29, 18:18
conference contribution
posted on 2023-12-11, 20:14 authored by Tom Horak, Norine CoenenNorine Coenen, Niklas MetzgerNiklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd FinkbeinerBernd Finkbeiner, Raimund Dachselt
Model checkers provide algorithms for proving that a mathematical model of a system satisfies a given specification. In case of a violation, a counterexample that shows the erroneous behavior is returned. Understanding these counterexamples is challenging, especially for hyperproperty specifications, i.e., specifications that relate multiple executions of a system to each other. We aim to facilitate the visual analysis of such counterexamples through our HYPERVIS tool, which provides interactive visualizations of the given model, specification, and counterexample. Within an iterative and interdisciplinary design process, we developed visualization solutions that can effectively communicate the core aspects of the model checking result. Specifically, we introduce graphical representations of binary values for improving pattern recognition, color encoding for better indicating related aspects, visually enhanced textual descriptions, as well as extensive cross-view highlighting mechanisms. Further, through an underlying causal analysis of the counterexample, we are also able to identify values that contributed to the violation and use this knowledge for both improved encoding and highlighting. Finally, the analyst can modify both the specification of the hyperproperty and the system directly within HYPERVIS and initiate the model checking of the new version. In combination, these features notably support the analyst in understanding the error leading to the counterexample as well as iterating the provided system and specification. We ran multiple case studies with HYPERVIS and tested it with domain experts in qualitative feedback sessions. The participants’ positive feedback confirms the considerable improvement over the manual, text-based status quo and the value of the tool for explaining hyperproperties.

History

Preferred Citation

Tom Horak, Norine Coenen, Niklas Metzger, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner and Raimund Dachselt. Visual Analysis of Hyperproperties for Understanding Model Checking Results. In: IEEE Visualization Conference (VIS). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Visualization Conference (VIS)

Legacy Posted Date

2022-05-06

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3659, title = "Visual Analysis of Hyperproperties for Understanding Model Checking Results", author = "Horak, Tom and Coenen, Norine and Metzger, Niklas and Hahn, Christopher and Flemisch, Tamara and Méndez, Julián and Dimov, Dennis and Finkbeiner, Bernd and Dachselt, Raimund", booktitle="{IEEE Visualization Conference (VIS)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC