Abstract
Causality Checking [LL13] computes a causal explanation in the form of minimal action traces that lead to the violations of a reachability property. Causality Checking is implemented in the tool QuantUM [LFL11] that currently only depicts in a fault tree the causal actions in the action traces that lead to a property violation, but not the possible order of these actions. We present an analysis to compute the strict partial order of actions in action traces and succinctly depict these orders by a fault tree. We implemented the analysis in the tool QuantUM. We assess the performance of our algorithm by applying it to several models of different size. The results show that the analysis can compute the action order for thousands of action traces.
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
References
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Chartrand, G., Lesniak-Foster, L.: Graphs & Digraphs, 4th edn. Chapman and Hall/CRC, Boca Raton [u.a.] (2005)
Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)
Eppstein, D., Simons, J.A.: Confluent Hasse diagrams. J. Graph Algorithms Appl. 17(7), 689–710 (2013)
Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)
IBM Corp.: IBM SPSS Statistics for Windows, Version 27 (2020). https://www.ibm.com/analytics/spss-statistics-software
Kölbl, M., Leue, S.: An efficient algorithm for computing causal trace sets in causality checking. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 171–186. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_10
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Leitner-Fischer, F.: Causality checking of safety-critical software and systems. Ph.D. thesis, University of Konstanz, Germany (2015)
Lewis, D.: Counterfactuals. Wiley-Blackwell, London (2001)
Leitner-Fischer, F., Leue, S.: Quantum: quantitative safety analysis of UML models. In: Massink, M., Norman, G. (eds.) QAPL, volume 57 of EPTCS, pp. 16–30 (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). https://doi.org/10.1007/978-3-642-35873-9_16
Object Management Group: OMG Systems Modeling Language, Specification 1.5 (2017). http://www.omg.org/spec/SysML
O’Neil, P.E., O’Neil, E.J.: A fast expected time algorithm for Boolean matrix multiplication and transitive closure. Inf. Control 22(2), 132–138 (1973)
Steffen, B., Rüthing, O., Huth, M.: Mathematical Foundations of Advanced Informatics, Volume 1: Inductive Approaches. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-68397-3
Weiser, J.: Derivation of a minimal representation of incomplete partial orders from event sequences. Master’s thesis, University of Konstanz (2019)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Kölbl, M., Leue, S. (2021). An Algorithm to Compute a Strict Partial Ordering of Actions in Action Traces. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. ISoLA 2020. Lecture Notes in Computer Science(), vol 12479. Springer, Cham. https://doi.org/10.1007/978-3-030-83723-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-83723-5_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-83722-8
Online ISBN: 978-3-030-83723-5
eBook Packages: Computer ScienceComputer Science (R0)