Causality analysis and fault ascription in component-based systems

被引:11
作者
Gassler, Gregor [1 ]
Stefani, Jean-Bernard [1 ]
机构
[1] Univ Grenoble Alpes, INRIA, CNRS, Grenoble INP,LIG, F-38000 Grenoble, France
关键词
Causality; Counterfactual analysis; Formal requirements; Components; Hyperproperties; DIAGNOSIS;
D O I
10.1016/j.tcs.2020.06.010
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This article introduces a general framework for fault ascription, which consists in identifying, within a multi-component system, the components whose faulty behavior has caused the failure of said system. Our framework uses configuration structures as a general semantical model to handle truly concurrent executions, partial and distributed observations in a uniform way. As a first contribution, and in contrast with most of the current literature on counterfactual analysis which relies heavily on a set of toy examples, we first define a set of expected formal properties for counterfactual builders, i.e. operators that build counterfactual executions. We then show that causality analyses that satisfy our requirements meet a set of elementary soundness and completeness properties. Finally we present a concrete causality analysis meeting all our requirements, and we show that it behaves well under refinement. We present several examples illustrating various phenomena such as causal over-determination or observational determinism, and we discuss the relationship of our approach with Halpern and Pearl's actual causality analysis. (c) 2020 Elsevier B.V. All rights reserved.
引用
收藏
页码:158 / 180
页数:23
相关论文
共 39 条
  • [1] Baldan P., 2008, LNCS, V5201
  • [2] BALKE A, 1994, PROCEEDINGS OF THE TWELFTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOLS 1 AND 2, P230
  • [3] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    [J]. MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
  • [4] Explaining counterexamples using causality
    Beer, Ilan
    Ben-David, Shoham
    Chockler, Hana
    Orni, Avigail
    Trefler, Richard
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) : 20 - 40
  • [5] Benveniste A., 2003, LNCS, V2761
  • [6] Cassandras C. G., 2007, INTRO DISCRETE EVENT, V2nd
  • [7] Hyperproperties
    Clarkson, Michael
    Schneider, Fred
    [J]. JOURNAL OF COMPUTER SECURITY, 2010, 18 (06) : 1157 - 1210
  • [8] Program Actions as Actual Causes: A Building Block for Accountability
    Datta, Anupam
    Garg, Deepak
    Kaynar, Dilsun
    Sharma, Divya
    Sinha, Arunesh
    [J]. 2015 IEEE 28TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM CSF 2015, 2015, : 261 - 275
  • [9] On Preemption and Overdetermination in Formal Theories of Causality
    Dyrkolbotn, Sjur K.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (259): : 1 - 15
  • [10] Esparza J., 1999, LECT NOTES COMPUTER, V1664