Sorry, this content is only available in English. For your convenience, it is shown below in this language.
Visual Analysis of Hyperproperties for Understanding Model Checking Results
Product of a collaboration between the IMLD (with Tom Horak, Tamara Flemisch, Julian Méndez, Dennis Dimov, and Raimund Dachselt) and the Reactive Systems Group, the HyperVis tool enables visual analysis of counterexamples to hyperproperties, which are traditionally complex text-based outputs from model checking console applications. We achieved this by providing interactive visualizations of the given model, specifications that it must comply to, and counterexamples, in case they exist. The users are guided to effectively understand the counterexample, and then to repair either the model or the specification. Understanding is supported through encoding of binary values for pattern recognition and linked interactions of several views to encode and highlight relevant aspects of the counterexample, to eventually find the cause of the violation. The iterative repair process is supported by dedicated editing interfaces for temporal logics and transition systems, project versioning and management. Supported by several real life use cases in it’s qualitative evaluation, domain experts confirmed the improvement it presents over the existing text-based solutions and its value for explainability of hyperproperties.
A Visualization Authoring Model for Post-WIMP Interfaces
In this work, Marc Satkowski, Weizhou Luo, and Raimund Dachselt focus on the problem, that Authoring AR visualizations still heavily relies on stationary desktop setups, which inevitably separates users from the actual working space the created visualizations should be used in. To adapt to the changes of Post-WIMP Interfaces, the presented model emphasizes the iterative nature of creating and configuring visualizations, the existence of multiple views in the same system, and requirements for the data analysis process.
Contributions at VIS 2021
@article{Horak2021VisualAnalysisHyperproperties,
author = {Tom Horak and Norine Coenen and Niklas Metzger and Christopher Hahn and Tamara Flemisch and Juli\'{a}n M\'{e}ndez and Dennis Dimov and Bernd Finkbeiner and Raimund Dachselt},
title = {Visual Analysis of Hyperproperties for Understanding Model Checking Results},
journal = {IEEE Transactions on Visualization and Computer Graphics},
year = {2022},
month = {10},
location = {Virtual Event},
doi = {10.1109/TVCG.2021.3114866},
publisher = {IEEE}
}List of additional material
, Video, Online Demo
@inproceedings{satkowski2021visualization,
author = {Marc Satkowski and Weizhou Luo and Raimund Dachselt},
title = {A Visualization Authoring Model for Post-WIMP Interfaces},
booktitle = {Poster Program of the 2021 IEEE VIS Conference},
year = {2021},
month = {10},
location = {Virtual Event},
numpages = {2},
doi = {10.48550/arXiv.2110.14312},
url = {https://arxiv.org/abs/2110.14312}
}List of additional material
