Skip to main content
Top

2015 | OriginalPaper | Chapter

A Hybrid Approach to Causality Analysis

Authors : Shaohui Wang, Yoann Geoffroy, Gregor Gössler, Oleg Sokolsky, Insup Lee

Published in: Runtime Verification

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In component-based safety-critical systems, when a system safety property is violated, it is necessary to analyze which components are the cause. Given a system execution trace that exhibits component faults leading to a property violation, our causality analysis formalizes a notion of counterfactual reasoning (“what would the system behavior be if a component had been correct?”) and algorithmically derives such alternative system behaviors, without re-executing the system itself. In this paper, we show that we can improve precision of the analysis if (1) we can emulate execution of components instead of relying on their contracts, and (2) take into consideration input/output dependencies between components to avoid blaming components for faults induced by other components. We demonstrate the utility of the extended analysis with a case study for a closed-loop patient-controlled analgesia system.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Throughout the paper we use bold font to represent a set of traces (e.g., \(\mathbf {TR}\), \(\mathbf {T}_{X}\)) or a property (e.g., \(\mathbf P\)) and calligraphic font to represent a set of components (e.g., \(\mathcal A\) in Definition 3).
 
Literature
1.
go back to reference Arney, D., Pajic, M., Goldman, J.M., Lee, I., Mangharam, R., Sokolsky, O.: Toward patient safety in closed-loop medical device systems. In: ICCPS 2010, pp. 139–148. ACM, New York, NY, USA (2010) Arney, D., Pajic, M., Goldman, J.M., Lee, I., Mangharam, R., Sokolsky, O.: Toward patient safety in closed-loop medical device systems. In: ICCPS 2010, pp. 139–148. ACM, New York, NY, USA (2010)
2.
go back to reference ASTM International. F2761–2009. Medical Devices and Medical Systems – Essential Safety Requirements for Equipment Comprising the Patient-Centric Integrated Clinical Environment (ICE), Part 1, 2009 ASTM International. F2761–2009. Medical Devices and Medical Systems – Essential Safety Requirements for Equipment Comprising the Patient-Centric Integrated Clinical Environment (ICE), Part 1, 2009
3.
go back to reference Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 94–108. Springer, Heidelberg (2009) CrossRef Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 94–108. Springer, Heidelberg (2009) CrossRef
4.
go back to reference Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. SIGSOFT Softw. Eng. Notes 29(6), 73–82 (2004)CrossRef Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. SIGSOFT Softw. Eng. Notes 29(6), 73–82 (2004)CrossRef
5.
go back to reference de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artif. Intell. 32(1), 97–130 (1987)CrossRefMATH de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artif. Intell. 32(1), 97–130 (1987)CrossRefMATH
6.
go back to reference de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRef de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRef
7.
go back to reference Gössler, G., Aştefănoaei, L.: Blaming in component-based real-time systems. In: Proceedings of the 14th International Conference on Embedded Software (2014) Gössler, G., Aştefănoaei, L.: Blaming in component-based real-time systems. In: Proceedings of the 14th International Conference on Embedded Software (2014)
8.
go back to reference Gössler, G., Le Métayer, D.: A general trace-based framework of logical causality. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 157–173. Springer, Heidelberg (2014) Gössler, G., Le Métayer, D.: A general trace-based framework of logical causality. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 157–173. Springer, Heidelberg (2014)
9.
go back to reference Gössler, G., Le Métayer, D., Raclet, J.-B.: Causality analysis in contract violation. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 270–284. Springer, Heidelberg (2010) CrossRef Gössler, G., Le Métayer, D., Raclet, J.-B.: Causality analysis in contract violation. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 270–284. Springer, Heidelberg (2010) CrossRef
10.
go back to reference Halpern, Y.P., Pearl, J.: Causes and explanations: a structural-model approach. Part I: causes. Br. J. Philos. Sci. 56(4), 743–887 (2005)MATH Halpern, Y.P., Pearl, J.: Causes and explanations: a structural-model approach. Part I: causes. Br. J. Philos. Sci. 56(4), 743–887 (2005)MATH
11.
go back to reference Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. SIGPLAN Not. 46(6), 437–446 (2011)CrossRef Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. SIGPLAN Not. 46(6), 437–446 (2011)CrossRef
12.
go back to reference King, A., Procter, S., Andresen, D., Hatcliff, J., Warren, S., Spees, W., Jetley, R.P., Jones, P.L., Weininger, S.: An open test bed for medical device integration and coordination. In: ICSE Companion, pp. 141–151. IEEE (2009) King, A., Procter, S., Andresen, D., Hatcliff, J., Warren, S., Spees, W., Jetley, R.P., Jones, P.L., Weininger, S.: An open test bed for medical device integration and coordination. In: ICSE Companion, pp. 141–151. IEEE (2009)
13.
go back to reference Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 71–84. Springer, Heidelberg (2011) CrossRef Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 71–84. Springer, Heidelberg (2011) CrossRef
14.
go back to reference Leitner-Fischer, F., Leue, S.: On the synergy of probabilistic causality computation and causality checking. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 246–263. Springer, Heidelberg (2013) CrossRef Leitner-Fischer, F., Leue, S.: On the synergy of probabilistic causality computation and causality checking. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 246–263. Springer, Heidelberg (2013) CrossRef
15.
go back to reference Lewis, D.: Counterfactuals, 2nd edn. Wiley-Blackwell, New York (2001) MATH Lewis, D.: Counterfactuals, 2nd edn. Wiley-Blackwell, New York (2001) MATH
17.
go back to reference Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: ASE 2003, pp. 30–39 (2003) Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: ASE 2003, pp. 30–39 (2003)
18.
go back to reference Wang, S., Ayoub, A., Ivanov, R., Sokolsky, O., Lee, I.: Contract-based blame assignment by trace analysis. In: HiCoNS 2013, pp. 117–125 (2013) Wang, S., Ayoub, A., Ivanov, R., Sokolsky, O., Lee, I.: Contract-based blame assignment by trace analysis. In: HiCoNS 2013, pp. 117–125 (2013)
19.
go back to reference Wang, S., Ayoub, A., Kim, B.G., Gössler, G., Sokolsky, O., Lee, I.: A causality analysis framework for component-based real-time systems. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 285–303. Springer, Heidelberg (2013) CrossRef Wang, S., Ayoub, A., Kim, B.G., Gössler, G., Sokolsky, O., Lee, I.: A causality analysis framework for component-based real-time systems. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 285–303. Springer, Heidelberg (2013) CrossRef
20.
go back to reference Zeller, A.: Isolating cause-effect chains from computer programs. In: ACM International Symposium on Foundations of Software Engineering, pp. 1–10 (2002) Zeller, A.: Isolating cause-effect chains from computer programs. In: ACM International Symposium on Foundations of Software Engineering, pp. 1–10 (2002)
Metadata
Title
A Hybrid Approach to Causality Analysis
Authors
Shaohui Wang
Yoann Geoffroy
Gregor Gössler
Oleg Sokolsky
Insup Lee
Copyright Year
2015
DOI
https://doi.org/10.1007/978-3-319-23820-3_16

Premium Partner