Explaining Hyperproperty Violations

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

  • Norine Coenen - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Raimund Dachselt - , Professur für Multimedia-Technologie (MT) (Autor:in)
  • Bernd Finkbeiner - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Hadar Frenkel - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Christopher Hahn - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Tom Horak - , elevait GmbH & Co. KG (Autor:in)
  • Niklas Metzger - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)
  • Julian Siber - , CISPA – Helmholtz-Zentrum für Informationssicherheit (Autor:in)

Abstract

Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in the system that led to the counterexample is a difficult manual effort that highly benefits from additional explanations. In this paper, we present an explanation method for counterexamples to hyperproperties described in the specification logic HyperLTL. We extend Halpern and Pearl’s definition of actual causality to sets of traces witnessing the violation of a HyperLTL formula, which allows us to identify the events that caused the violation. We report on the implementation of our method and show that it significantly improves on previous approaches for analyzing counterexamples returned by HyperLTL model checkers.

Details

OriginalspracheEnglisch
TitelComputer Aided Verification
Redakteure/-innenSharon Shoham, Yakir Vizel
Herausgeber (Verlag)Springer Science and Business Media B.V.
Seiten407-429
Seitenumfang23
ISBN (elektronisch)978-3-031-13185-1
ISBN (Print)978-3-031-13184-4
PublikationsstatusVeröffentlicht - 2022
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band13371 LNCS
ISSN0302-9743

Konferenz

Titel34th International Conference on Computer Aided Verification, CAV 2022
Dauer7 - 10 August 2022
StadtHaifa
LandIsrael

Externe IDs

ORCID /0000-0002-2176-876X/work/159171489

Schlagworte