Abstract
In recent years, several approaches to generate probabilistic counterexamples have been proposed. The interpretation of stochastic counterexamples, however, continues to be problematic since they have to be represented as sets of paths, and the number of paths in this set may be very large. Fault trees (FTs) are a well-established industrial technique to represent causalities for possible system hazards resulting from system or system component failures. In this paper we suggest a method to automatically derive FTs from counterexamples, including a mapping of the probability information onto the FT. We extend the structural equation approach by Pearl and Halpern, which is based on Lewis counterfactuals, so that it serves as a justification for the causality that our proposed FT derivation rules imply. We demonstrate the usefulness of our approach by applying it to an industrial case study.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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, Los Alamitos (2009)
Aljazzar, H., Leue, S.: Debugging of Dependability Models Using Interactive Visualization of Counterexamples. In: Proc. of QEST 2008. IEEE Computer Society, Los Alamitos (2008)
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)
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)
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)
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)
Chen, B., Avrunin, G., Clarke, L., Osterweil, L.: Automatic Fault Tree Derivation From Little-Jil Process Definitions. In: Wang, Q., Pfahl, D., Raffo, D.M., Wernick, P. (eds.) SPW 2006 and ProSim 2006. LNCS, vol. 3966, pp. 150–158. Springer, Heidelberg (2006)
Collins, J. (ed.): Causation and Counterfactuals. MIT Press, Cambridge (2004)
Dugan, J., Bavuso, S., Boyd, M.: Dynamic Fault Tree Models for Fault Tolerant Computer Systems. IEEE Trans. Reliability (1992)
Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. Artificial Intelligence (2002)
Halpern, J., Pearl, J.: Causes and explanations: A structural-model approach. Part I: Causes. The British Journal for the Philosophy of Science (2005)
Han, T., Katoen, J.-P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. (2009)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. Technical Report soft-11-02, Chair for Software Engineering, University of Konstanz (2011), http://www.inf.uni-konstanz.de/soft/research/publications/pdf/soft-11-02.pdf
Leitner-Fischer, F., Leue, S.: QuantUM: Quantitative safety analysis of UML models. In: Proc. of QAPL 2011 (2011)
Lewis, D.: Counterfactuals. Wiley-Blackwell, Chichester (2001)
McKelvin Jr, M., Eirea, G., Pinello, C., Kanajan, S., Sangiovanni-Vincentelli, A.: A Formal Approach to Fault Tree Synthesis for the Analysis of Distributed Fault Tolerant Systems. In: Proc. of EMSOFT 2005. ACM, New York (2005)
Pai, G., Dugan, J.: Automatic synthesis of dynamic fault trees from UML system models. In: Proc. of ISSRE 2002. IEEE Computer Society, Los Alamitos (2002)
Schellhorn, G., Thums, A., Reif, W.: Formal fault tree semantics. In: Proc. IDPT 2002. Society for Design and Process Science (2002)
U.S. Nuclear Regulatory Commission. Fault Tree Handbook, NUREG-0492 (1981)
Zeller, A.: Why Programs Fail: A Guide to Systematic Debugging. Elsevier, Amsterdam (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuntz, M., Leitner-Fischer, F., Leue, S. (2011). From Probabilistic Counterexamples via Causality to Fault Trees. In: Flammini, F., Bologna, S., Vittorini, V. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2011. Lecture Notes in Computer Science, vol 6894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24270-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-24270-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24269-4
Online ISBN: 978-3-642-24270-0
eBook Packages: Computer ScienceComputer Science (R0)