Abstract
In component-based safety-critical embedded systems it is crucial to determine the cause(s) of the violation of a safety property, be it to issue a precise alert, to steer the system into a safe state, or to determine liability of component providers. In this paper we present an approach to blame components based on a single execution trace violating a safety property \(P\). The diagnosis relies on counterfactual reasoning (“what would have been the outcome if component \(C\) had behaved correctly?”) to distinguish component failures that actually contributed to the outcome from failures that had little or no impact on the violation of \(P\).
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
Similar content being viewed by others
Notes
- 1.
It is straight-forward to allow for additional information in traces \(tr\in B\) that is not observable in the log, by adding to the cartesian product of \(\varSigma \) another alphabet that does not appear in the projections. For instance, events may be recorded with some timing uncertainty rather than precise time stamps [23].
- 2.
For the sake of readability we omit the prefix closure of the specifications in the examples.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)
Beckers, S., Vennekens, J.: Counterfactual dependency and actual causation in cp-logic and structural models: a comparison. In: Kersting, K., Toussaint, M. (eds.) STAIRS. Frontiers in Artificial Intelligence and Applications, vol. 241, pp. 35–46. IOS Press (2012)
Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterexamples using causality. Formal Methods Syst. Des. 40(1), 20–40 (2012)
Fabre, E., Benveniste, A., Haar, S., Jard, C.: Distributed monitoring of concurrent and asynchronous systems. Discrete Event Dyn. Syst. 15(1), 33–84 (2005)
Fey, G., Staber, S., Bloem, R., Drechsler, R.: Automatic fault localization for property checking. IEEE Trans. CAD Integr. Circ. Syst. 27(6), 1138–1149 (2008)
Fidge, C.J.: Timestamps in message-passing systems that preserve the partial ordering. In: Raymond, K. (ed.) Proceedings of the ACSC’88, pp. 56–66 (1988)
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)
Gössler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Prog. 55(1–3), 161–183 (2005)
Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. STTT 8(3), 229–247 (2006)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991)
Halpern, J.Y., Pearl, J.: Causes and explanations: a structural-model approach. part I: Causes. Br. J. Philos. Sci. 56(4), 843–887 (2005)
Hume, D.: An Enquiry Concerning Human Understanding (1748)
Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012)
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)
Küsters, R., Truderung, T., Vogt, A.: Accountability: definition and relationship to verifiability. In: ACM Conference on Computer and Communications Security, pp. 526–535 (2010)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. CACM 21(7), 558–565 (1978)
Lee, E.A., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 17(12), 1217–1229 (1998)
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)
Mattern, F.: Virtual time and global states of distributed systems. In: Cosnard, M. (ed.) Proceedings of the Workshop on Parallel and Distributed Algorithms, pp. 215–226. Elsevier (1988)
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)
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)
Wang, S., Ayoub, A., Sokolsky, O., Lee, I.: Runtime verification of traces under recording uncertainty. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 442–456. Springer, Heidelberg (2012)
Zeller, A.: Why Programs Fail. Elsevier, Amsterdam (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gössler, G., Le Métayer, D. (2014). A General Trace-Based Framework of Logical Causality. In: Fiadeiro, J., Liu, Z., Xue, J. (eds) Formal Aspects of Component Software. FACS 2013. Lecture Notes in Computer Science(), vol 8348. Springer, Cham. https://doi.org/10.1007/978-3-319-07602-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-07602-7_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07601-0
Online ISBN: 978-3-319-07602-7
eBook Packages: Computer ScienceComputer Science (R0)