English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Model checkers provide algorithms for proving that a mathematical model of asystem satisfies a given specification. In case of a violation, acounterexample that shows the erroneous behavior is returned. Understandingthese counterexamples is challenging, especially for hyperpropertyspecifications, i.e., specifications that relate multiple executions of asystem to each other. We aim to facilitate the visual analysis of suchcounterexamples through our HyperVis tool, which provides interactivevisualizations of the given model, specification, and counterexample. Within aniterative and interdisciplinary design process, we developed visualizationsolutions that can effectively communicate the core aspects of the modelchecking result. Specifically, we introduce graphical representations of binaryvalues for improving pattern recognition, color encoding for better indicatingrelated aspects, visually enhanced textual descriptions, as well as extensivecross-view highlighting mechanisms. Further, through an underlying causalanalysis of the counterexample, we are also able to identify values thatcontributed to the violation and use this knowledge for both improved encodingand highlighting. Finally, the analyst can modify both the specification of thehyperproperty and the system directly within HyperVis and initiate the modelchecking of the new version. In combination, these features notably support theanalyst in understanding the error leading to the counterexample as well asiterating the provided system and specification. We ran multiple case studieswith HyperVis and tested it with domain experts in qualitative feedbacksessions. The participants' positive feedback confirms the considerableimprovement over the manual, text-based status quo and the value of the toolfor explaining hyperproperties.

Visual Analysis of Hyperproperties for Understanding Model Checking Results