Abstract
In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In this paper we combine the strengths of both approaches and propose an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events. We demonstrate the increase in performance of our approach using several case studies.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying Continuous-Time Markov Chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
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: Proc. of QEST 2009. IEEE Computer Society (2009)
Aljazzar, H., Leitner-Fischer, F., Leue, S., Simeonov, D.: DiPro - A tool for probabilistic counterexample generation. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 183–187. Springer, Heidelberg (2011)
Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Soft. Eng. (2009)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Soft. Eng. (2003)
Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)
Böde, E., Peikenkamp, T., Rakow, J., Wischmeyer, S.: Model Based Importance Analysis for Minimal Cut Sets. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 303–317. Springer, Heidelberg (2008)
Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Transactions on Dependable and Secure Computing 7(2), 128–143 (2010)
Brzozowski, J.A., Leiss, E.: On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science 10(1), 19–35 (1980)
Chandra, A.K., Stockmeyer, L.J.: Alternation. In: 17th Annual Symposium on Foundations of Computer Science, pp. 98–108. IEEE (1976)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, 3rd edn. The MIT Press (2001)
Collins, J. (ed.): Causation and Counterfactuals. MIT Press (2004)
de Jonge, M., Ruys, T.C.: The spinJa model checker. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 124–128. Springer, Heidelberg (2010)
Dugan, J., Bavuso, S., Boyd, M.: Dynamic Fault Tree Models for Fault Tolerant Computer Systems. IEEE Trans. Reliability (1992)
Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods in System Design 24(2), 101–127 (2004)
Halpern, J., Pearl, J.: Causes and explanations: A structural-model approach. Part I: Causes. The British Journal for the Phil. of Science (2005)
Han, T., Katoen, J.-P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. (2009)
Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: The prism language - semantics, http://www.prismmodelchecker.org/doc/semantics.pdf
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addision–Wesley (2003)
Kulkarni, V.: Modeling and analysis of stochastic systems. Chapman & Hall/CRC (1995)
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)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST 2012), pp. 203–204. IEEE CS Press (2012)
Leitner-Fischer, F., Leue, S.: QuantUM: Quantitative safety analysis of UML models. In: Proc. of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL 2011) (2011)
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)
Leitner-Fischer, F., Leue, S.: On the synergy of probabilistic causality computation and causality checking. Technical Report soft-13-01, Chair for Software Engineering, University of Konstanz (2013), http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-13-01.pdf
Lewis, D.: Counterfactuals. Wiley-Blackwell (2001)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer-Verlag New York, Inc. (1992)
Muppala, J., Ciardo, G., Trivedi, K.: Stochastic reward nets for reliability prediction. Communications in Reliability, Maintainability and Serviceability 1(2), 9–20 (1994)
Power, C., Miller, A.: Prism2promela. In: Fifth International Conference on Quantitative Evaluation of Systems, QEST 2008, pp. 79–80. IEEE (2008)
U.S. Nuclear Regulatory Commission. Fault Tree Handbook (1981)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Wimmer, R., Jansen, N., Ábrahám, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time markov models. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299–314. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leitner-Fischer, F., Leue, S. (2013). On the Synergy of Probabilistic Causality Computation and Causality Checking. In: Bartocci, E., Ramakrishnan, C.R. (eds) Model Checking Software. SPIN 2013. Lecture Notes in Computer Science, vol 7976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39176-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-39176-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39175-0
Online ISBN: 978-3-642-39176-7
eBook Packages: Computer ScienceComputer Science (R0)