论文标题
解释违反超副品的行为
Explaining Hyperproperty Violations
论文作者
论文摘要
HyperProperties将多个计算轨迹相互关联。因此，模型的超版本的模型棋子返回，如果系统模型违反了规范，则一组迹线作为反例。固定导致反例的系统痕迹之间的错误关系是一项艰难的手动努力，从其他解释中受益匪浅。在本文中，我们提出了一种对规范逻辑超ltl中描述的反典范的反例的解释方法。我们将Halpern和Pearl对实际因果关系的定义扩展到目睹违反HyperLTL公式的一组痕迹，这使我们能够确定造成违法行为的事件。我们报告了我们方法的实现，并表明它可以显着改善以前的方法，用于分析HyperLTL模型检查器返回的反例。
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.
