Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
String Analysis for Vulnerability Detection and Repair Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Symbolic Causality Checking Using Bounded Model Checking

Authors : Adrian Beer, Stephan Heidinger, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue

Published in: Model Checking Software

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

In precursory work we have developed causality checking, a fault localization method for concurrent system models relying on the Halpern and Pearl counterfactual model of causation that identifies ordered occurrences of system events as being causal for the violation of non-reachability properties. Our first implementation of causality checking relies on explicit-state model checking. In this paper we propose a symbolic implementation of causality checking based on bounded model checking (BMC) and SAT solving. We show that this BMC-based implementation is efficient for large and complex system models. The technique is evaluated on industrial size models and experimentally compared to the existing explicit state causality checking implementation. BMC-based causality checking turns out to be superior to the explicit state variant in terms of runtime and memory consumption for very large system models.

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!

inform now

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!

inform now

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!

inform now
previous chapter PickLock: A Deadlock Prediction Approach under Nested Locking
next chapter Model Counting for Complex Data Structures
Literature
1.
Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner-Fischer, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counterexamples. In: Proceedings of the QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems. IEEE Computer Society (2009)
2.
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, New York (2008)MATH
3.
4.
5.
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
6.
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999) CrossRef
7.
Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 162–176. Springer, Heidelberg (2007) CrossRef
8.
Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49–62. Springer, Heidelberg (2003) CrossRef
9.
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002) CrossRef
10.
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
11.
Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transfer (STTT) 8(3), 229–247 (2006)CrossRef
12.
Halpern, J., Pearl, J.: Causes and explanations: A structural-model approach. Causes. Br. J. Philos. Sci., Part I 56, 843–887 (2005)MATHMathSciNetCrossRef
13.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addision-Wesley, Reading (2003)
14.
de Jonge, M., Ruys, T.C.: The SpinJa model checker. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 124–128. Springer, Heidelberg (2010) CrossRef
15.
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
16.
17.
Leitner-Fischer, F., Leue, S.: QuantUM: Quantitative safety analysis of UML models. In: Proceedings Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011). EPTCS, vol. 57, pp. 16–30 (2011)
18.
Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 248–267. Springer, Heidelberg (2013) CrossRef
19.
Leitner-Fischer, F., Leue, S.: Probabilistic fault tree synthesis using causality computation. Int. J. Critical Comput.-Based Syst. 4, 119–143 (2013)CrossRef
20.
Leitner-Fischer, F., Leue, S.: Spincause: A tool for causality checking. In: Proceedings of the International SPIN Symposium on Model Checking of Software (SPIN 2014). ACM, San Jose (2014)
21.
Lewis, D.: Counterfactuals. Blackwell Publishers, Oxford (1973)
22.
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)
23.
Metadata
Title
Symbolic Causality Checking Using Bounded Model Checking
Authors
Adrian Beer
Stephan Heidinger
Uwe Kühne
Florian Leitner-Fischer
Stefan Leue
Copyright Year
2015
Book
Model Checking Software

Print ISBN: 978-3-319-23403-8

Electronic ISBN: 978-3-319-23404-5

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-23404-5_14

Premium Partner

    Image Credits