Abstract
Many safety critical systems guarantee fault-tolerance by using several redundant copies of their components. When designing such redundancy architectures, it is crucial to analyze their fault trees, which describe combinations of faults of individual components that may cause malfunction of the system. State-of-the-art techniques for fault tree computation use first-order formulas with uninterpreted functions to model the transformations of signals performed by the redundancy system and an AllSMT query for computation of the fault tree from this encoding. Scalability of the analysis can be further improved by techniques such as predicate abstraction, which reduces the problem to Boolean case.
In this paper, we show that as far as fault trees of redundancy architectures are concerned, signal transformation can be equivalently viewed in a purely Boolean way as fault propagation. This alternative view has important practical consequences. First, it applies also to general redundancy architectures with cyclic dependencies among components, to which the current state-of-the-art methods based on AllSMT are not applicable, and which currently require expensive sequential reasoning. Second, it allows for a simpler encoding of the problem and usage of efficient algorithms for analysis of fault propagation, which can significantly improve the runtime of the analyses. A thorough experimental evaluation demonstrates the superiority of the proposed techniques.
Chapter PDF
Similar content being viewed by others
References
Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-825
Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP safety analysis platform. In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms or the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9636, pp. 533–539. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_31
Bozzano, M., Cimatti, A., Griggio, A., Mattarei, C.: Efficient anytime techniques for model-based safety analysis. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9206, pp. 603–621. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_41
Bozzano, M., Cimatti, A., Mattarei, C.: Automated analysis of reliability architectures. In: 2013 18th International Conference on Engineering of Complex Computer Systems, Singapore, July 17-19, 2013. pp. 198–207. IEEE Computer Society (2013). https://doi.org/10.1109/ICECCS.2013.37
Bozzano, M., Cimatti, A., Mattarei, C.: Efficient analysis of reliability architectures via predicate abstraction. In: Bertacco, V., Legay, A. (eds.) Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings. Lecture Notes in Computer Science, vol. 8244, pp. 279–294. Springer (2013). https://doi.org/10.1007/978-3-319-03077-7_19
Bozzano, M., Cimatti, A., Mattarei, C.: Formal reliability analysis of redundancy architectures. Formal Aspects Comput. 31(1), 59–94 (2019). https://doi.org/10.1007/s00165-018-0475-1
Bozzano, M., Cimatti, A., Pires, A.F., Griggio, A., Jonáš, M., Kimberly, G.: Efficient SMT-Based Analysis of Failure Propagation. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 209–230. Springer (2021). https://doi.org/10.1007/978-3-030-81688-9_10
Bryant, R.E., German, S.M., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) Computer Aided Verification, 11th International Conference, CAV ’99, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol. 1633, pp. 470–482. Springer (1999). https://doi.org/10.1007/3-540-48683-6_40
Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: A tool for checking the refinement of temporal contracts. In: Denney, E., Bultan, T., Zeller, A. (eds.) 2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11-15, 2013. pp. 702–705. IEEE (2013). https://doi.org/10.1109/ASE.2013.6693137
Ding, K., Morozov, A., Janschek, K.: Classification of hierarchical fault-tolerant design patterns. In: 15th IEEE Intl Conf on Dependable, Autonomic and Secure Computing, 15th Intl Conf on Pervasive Intelligence and Computing, 3rd Intl Conf on Big Data Intelligence and Computing and Cyber Science and Technology Congress, DASC/PiCom/DataCom/CyberSciTech 2017, Orlando, FL, USA, November 6-10, 2017. pp. 612–619. IEEE Computer Society (2017). https://doi.org/10.1109/DASC-PICom-DataCom-CyberSciTec.2017.108
Dubslaff, C., Ding, K., Morozov, A., Baier, C., Janschek, K.: Breaking the limits of redundancy systems analysis. CoRR abs/1912.05364 (2019), http://arxiv.org/abs/1912.05364
Haeussermann, W.: Description and Performance of the Saturn Launch Vehicle’s Navigation, Guidance, and Control System. IFAC Proceedings Volumes 3(1), 275–312 (1970). https://doi.org/10.1016/S1474-6670(17)68785-8, 3rd International IFAC Conference on Automatic Control in Space, Toulouse, France, March 2-6, 1970
Hamamatsu, M., Tsuchiya, T., Kikuno, T.: On the Reliability of Cascaded TMR Systems. In: Ishikawa, Y., Tang, D., Nakamura, H. (eds.) 16th IEEE Pacific Rim International Symposium on Dependable Computing, PRDC 2010, Tokyo, Japan, December 13-15, 2010. pp. 184–190. IEEE Computer Society (2010). https://doi.org/10.1109/PRDC.2010.45
Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4144, pp. 424–437. Springer (2006). https://doi.org/10.1007/11817963_39
Lee, S., Jung, J., Lee, I.: Voting structures for cascaded triple modular redundant modules. IEICE Electronic Express 4(21), 657–664 (2007). https://doi.org/10.1587/elex.4.657
Prisaznuk, P.J.: Integrated modular avionics. In: Proceedings of the IEEE 1992 National Aerospace and Electronics Conference@ m\_NAECON 1992. pp. 39–45. IEEE (1992)
Ruijters, E., Stoelinga, M.: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29–62 (2015). https://doi.org/10.1016/j.cosrev.2015.03.001
Wynn, E.: A comparison of encodings for cardinality constraints in a SAT solver. CoRR abs/1810.12975 (2018), http://arxiv.org/abs/1810.12975
Yeh, Y.: Triple-triple redundant 777 primary flight computer. In: 1996 IEEE Aerospace Applications Conference. Proceedings. vol. 1, pp. 293–307 vol.1 (1996). https://doi.org/10.1109/AERO.1996.495891
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Bozzano, M., Cimatti, A., Griggio, A., Jonáš, M. (2022). Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)