Skip to main content
SpringerLink
Log in

Formal reliability analysis of redundancy architectures

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

Reliability is a fundamental property for critical systems. A thorough evaluation of the reliability is required by the certification procedures in various application domains, and it is important to support the exploration of the space of the design solutions. In this paper we propose a new, fully automated approach to the reliability analysis of complex redundant architectures. Given an abstract description of the architecture, the approach automatically extracts a fault tree and a symbolic reliability function, i.e. a program mapping the probability of fault of the basic components to the probability that the overall architecture deviates from the expected behavior. The proposed approach heavily relies on formal methods, by representing the architecture blocks as Uninterpreted Functions, and using the so-called miter construction to model the deviation from the nominal behavior. The extraction of all the deviation conditions is reduced to an AllSMT problem, and we extract the reliability function by traversing the Binary Decision Diagram corresponding to the quantified formula. Predicate abstraction is used to partition and speed up the computation. The approach has been implemented leveraging formal tools for model checking and safety assessment. A thorough experimental evaluation demonstrates its generality and effectiveness of the proposed techniques.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Akerlund O, Bieber P, Bde E, Bozzano M, Bretschneider M, Castel C, Cavallo A, Cifaldi M, Gauthier J, Griffault A, Lisagor O, Ludtke A, Metge S, Papadopoulos C, Peikenkamp T, Sagaspe L, Seguin C, Trivedi H, Valacca L (2006) ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proceedings of ERTS, Tolouse

  2. Anderson T, Lee PA (1981) Fault tolerance, principles and practice. Prentice/Hall International, Upper Saddle River

    MATH  Google Scholar 

  3. Abraham JA, Siewiorek DP (1974) An algorithm for the accurate reliability evaluation of triple modular redundancy networks. IEEE Trans Comput 23(7): 682–692

    Article  MATH  Google Scholar 

  4. Bozzano M, Bruttomesso R, Cimatti A, Junttila TA, van Rossum P, Schulz S, Sebastiani R (2005) MathSAT: tight integration of SAT and mathematical decision procedures. J Autom Reason 35(1-3): 265–293

    Article  MathSciNet  MATH  Google Scholar 

  5. Bittner B, Bozzano M, Cavada R, Cimatti A, Gario M, Griggio A, Mattarei C, Micheli A, Zampedri G (2016) The xSAP safety analysis platform. In: Proceedings of TACAS, vol 9636 of LNCS, pp 533–539

  6. Bruttomesso R, Cimatti A, Franzén A, Griggio A, Santuari A, Sebastiani R (2006) To Ackermann-ize or not to ackermann-ize? On efficiently handling uninterpreted function symbols in SMT(EUF). In: Hermann M, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning, 13th international conference, LPAR 2006, Phnom Penh, Cambodia, November 13–17, 2006, Proceedings, vol 4246 of lecture notes in computer science, Springer, pp 557–571

  7. Bozzano M, Cimatti A, Griggio A, Mattarei C (2015) Efficient anytime techniques for model-based safety analysis. In: Kroening D, Pasareanu CS (eds) Computer aided verification—27th international conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, vol 9206 of lecture notes in computer science, Springer, pp 603–621

  8. Bozzano M, Cimatti A, Katoen J-P, Nguyen VY, Noll T, Roveri M (2011) Safety, dependability and performance analysis of extended AADL models. Comput J 54(5): 754–775

    Article  Google Scholar 

  9. Bozzano M, Cimatti A, Katoen J-P, Katsaros P, Mokos K, Nguyen VY, Noll T, Postma B, Roveri M (2014) Spacecraft early design validation using formal methods. Reliab Eng Syst Saf 132: 20–35

    Article  Google Scholar 

  10. Bozzano M, Cimatti A, Lisagor O, Mattarei C, Mover S, Roveri M, Tonetta S (2011) Symbolic model checking and safety assessment of altarica models. Electron Commun EASST 46

  11. Bozzano M, Cimatti A, Fernandes Pires A, Jones D, Kimberly G, Petri T, Robinson R, Tonetta S (2015) Formal Design and Safety Analysis of AIR6110 Wheel Brake System. In: Proc. CAV, volume 9206 of LNCS, pp 518–535

  12. Bozzano M, Cimatti A, Tapparo F (2007) Symbolic fault tree analysis for reactive systems. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y (eds) Automated technology for verification and analysis, 5th international symposium, ATVA 2007, Tokyo, Japan, October 22–25, 2007, Proceedings, vol 4762 of lecture notes in computer science, Springer, pp 162–176

  13. Bensalem S, Ganesh V, Lakhnech Y, Munoz C, Owre S, Rueß H, Rushby J, Rusu V, Saıdi H, Shankar N et al (2000) An overview of SAL. In: Proceedings of the 5th NASA Langley formal methods workshop

  14. Bauer C, Lagadec K, Bès C, Mongeau M (2007) Flight control system architecture optimization for fly-by-wire airliners. J Guid Control Dyn 30(4): 1023–1029

    Article  Google Scholar 

  15. Brand D (1993) Verification of large synthesized designs. In: Proceedings of the 1993 IEEE/ACM international conference on computer-aided design, 1993, Santa Clara, California, USA, November 7–11, 1993, pp 534–537

  16. Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8): 677–691

    Article  MATH  Google Scholar 

  17. Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3): 293–318

    Article  MathSciNet  Google Scholar 

  18. Bruns G, Sutherland I (1997) Model checking and fault tolerance. In: International conference on algebraic methodology and software technology, Springer, pp 45–59

  19. Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule M, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185 of frontiers in artificial intelligence and applications, IOS Press, pp 825–885

  20. Bozzano M, Villafiorita A (2007) The FSAP/NuSMV-SA safety analysis platform. STTT 9(1): 5–24

    Article  Google Scholar 

  21. Bozzano M, Villafiorita A (2010) Design and safety assessment of critical systems: an Auerbach book. CRC Press, Boca Raton

    Book  Google Scholar 

  22. Bozzano M, Villafiorita A, Åkerlund O, Bieber P, Bougnol C, Böde E, Bretschneider M, Cavallo A et al (2003) ESACS: an integrated methodology for design and safety analysis of complex systems. In: Proceedings of ESREL 2003, Balkema Publisher, pp 237–245

  23. Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: Biere A, Bloem R (eds) Computer aided verification—26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, vol 8559 of lecture notes in computer science, Springer, pp 334–342

  24. Cavada R, Cimatti A, Franzén A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: Formal methods in computer-aided design, 7th international conference, FMCAD 2007, Austin, TX, USA, November 11–14, 2007, Proceedings, IEEE Computer Society, pp 69–76

  25. Cimatti A, Dorigatti M, Tonetta S (2013) 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, IEEE, pp 702–705

  26. Čepin M (2011) Reliability block diagram. In: Čepin M (ed) Assessment of power system reliability.. Springer, Berlin, pp 119–123

    Google Scholar 

  27. Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: Piterman N, Smolka S (eds) Tools and algorithms for the construction and analysis of systems—19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings, vol 7795 of lecture notes in computer science, Springer, pp 93–107

  28. Ciardo G, Muppala JK, Trivedi KS (1989) SPNP: stochastic petri net package. In: Petri nets and performance models, the proceedings of the third international workshop, PNPM ’89, Kyoto, Japan, December 11–13, 1989, IEEE Computer Society, pp 142–151

  29. International Business Machines Corporation (1964) SATURN V—launch vehicle digital computer: simplex models. Technical note NASA Part No. 50M35010, NASA

  30. Formal methods in computer-aided design, FMCAD 2007, Austin, Texas, USA, November 11–14, 2007, Proceedings of IEEE Computer Society, 2007

  31. Proceedings of 9th international conference on formal methods in computer-aided design, FMCAD 2009, 15–18 November 2009, Austin, TX, USA. IEEE, 2009

  32. Dutuit Y, Rauzy A (2001) New insights into the assessment of k-out-of-n and related systems. Reliab Eng Syst Saf 72(3): 303–314

    Article  Google Scholar 

  33. Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3-4): 209–236

    MATH  Google Scholar 

  34. Favalli M, Metra C (2004) TMR voting in the presence of crosstalk faults at the voter inputs. IEEE Trans Reliab 53(3): 342–348

    Article  Google Scholar 

  35. Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: Grumberg O (ed) Computer aided verification, 9th international conference, CAV ’97, Haifa, Israel, June 22–25, 1997, Proceedings, vol 1254 of lecture notes in computer science, Springer, pp 72–83

  36. Hinton A, Kwiatkowska MZ, Norman G, Parker D (2006) PRISM: a tool for automatic verification of probabilistic systems. In: Holger H, Jens P (eds) Tools and algorithms for the construction and analysis of systems, 12th international conference, TACAS 2006 held as part of the joint European conferences on theory and practice of software, ETAPS 2006, Vienna, Austria, March 25–April 2, 2006, Proceedings, vol 3920 of lecture notes in computer science, Springer, pp 441–444

  37. Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5): 279–295

    Article  Google Scholar 

  38. Hamamatsu M, Tsuchiya T, Kikuno T (2010) 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, IEEE Computer Society, pp 184–190

  39. Janowski T (1997) On bisimulation, fault-monotonicity and provable fault-tolerance. In: International conference on algebraic methodology and software technology, Springer, pp 292–306

  40. Joshi A, Heimdahl MPE (2005) Model-based safety analysis of simulink models using SCADE design verifier. In: Winther R, Gran BA, Dahll G (eds) Computer safety, reliability, and security, 24th international conference, SAFECOMP 2005, Fredrikstad, Norway, September 28–30, 2005, Proceedings, vol 3688 of lecture notes in computer science, Springer, pp 122–135

  41. Jones G, Sheeran M (1991) Relations and refinement in circuit design. In: Proceedings of the BCS FACS workshop on refinement, workshops in computing, Springer, pp 133–152

  42. Johnson JM, Wirthlin MJ (2010) Voter insertion algorithms for FPGA designs using Triple Modular Redundancy. In: Cheung PYK, Wawrzynek J (eds) Proceedings of the ACM/SIGDA 18th international symposium on field programmable gate arrays, FPGA 2010, Monterey, CA, USA, February 21–23, 2010, ACM, pp 249–258

  43. Joshi A, Heimdahl MPE, Miller SP, Whalen M (2006) Model-based safety analysis. NASA/CR-2006-213953

  44. Koren I, Krishna CM (2007) Fault-tolerant systems. Morgan-Kaufman, Burlington

    MATH  Google Scholar 

  45. Katoen J-P, Khattri M, Zapreev IS (2005) A Markov reward model checker. In: Second international conference on the quantitative evaluaiton of systems (QEST 2005), 19–22 September 2005, Torino, Italy, IEEE Computer Society, pp 243–244

  46. LayerZero Power Systems, Inc. https://www.layerzero.com/innovations/Industry-Firsts/index.html

  47. Lee S, Jung J, Lee I (2007) Voting structures for cascaded triple modular redundant modules. IEICE Electron Expr 4(21): 657–664

    Article  Google Scholar 

  48. Lahiri SK, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: Ball T, Jones RB (eds) Computer aided verification, 18th international conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, vol 4144 of lecture notes in computer science, Springer, pp 424–437

  49. Lanfang T, Qingping T, Jianli L (2011) Specification and verification of the triple-modular redundancy fault tolerant system using CSP. In: Proceedings of the fourth international conference on dependability (DEPEND), IARIA, pp 14–17

  50. Lahiri SK, Seshia SA (2004) The UCLID decision procedure. In: Alur R, Peled DA (eds) Computer aided verification, 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004, Proceedings, vol 3114 of lecture notes in computer science, Springer, pp 475–478

  51. Mattarei C (2016) Scalable safety and reliability analysis via symbolic model checking: theory and applications. Ph.D. thesis, University of Trento, Trento, Italy, p 2

  52. Mavridou A, Baranov E, Bliudze S, Sifakis J (2015) Configuration logics: modelling architecture styles. In: Braga C, Csaba ÖP (eds) Formal aspects of component software—12th international conference, FACS 2015, Niterói, Brazil, October 14–16, 2015, Revised Selected Papers, vol 9539 of lecture notes in computer science, Springer, pp 256–274

  53. McMillan KL (2007) Interpolants and symbolic model checking. In: Cook B, Podelski A (eds) Verification, model checking, and abstract interpretation, 8th international conference, VMCAI 2007, Nice, France, January 14–16, 2007, Proceedings, vol 4349 of lecture notes in computer science, Springer, pp 89–90

  54. Mongardi G (1993) Dependable computing for railway control systems. In: Landwehr CE, Randell B, Simoncini L (eds) Dependable computing for critical applications, vol 3. Springer, Vienna, pp 255–277

  55. Ranjan RK, Aziz A, Brayton RK, Pixley C, Plessier B (1995) Efficient bdd algorithms for synthesizing and verifying finite state machines. In: Proceedings of the IEEE/ACM international workshop on logic synthesis (IWLS95), Lake Tahoe (NV)

  56. Rauzy A (1993) New algorithms for fault trees analysis. Reliab Eng Syst Saf 40(3): 203–211

    Article  Google Scholar 

  57. Rauzy A (2001) Mathematical foundations of minimal cutsets. IEEE Trans Reliab 50(4): 389–396

    Article  Google Scholar 

  58. Sanders William H, Obal WD II, Qureshi MA, Widjanarko FK (1995) The UltraSAN modeling environment. Perform Eval 24(1-2): 89–115

    Article  MATH  Google Scholar 

  59. Marques SJP, Lynce I, Malik S (2009) Conflict-driven clause learning SAT solvers. In: Biere A, Heule M, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185 of frontiers in artificial intelligence and applications, IOS Press, pp 131–153

  60. Somenzi F (1998) CUDD: CU decision diagram package release 2.3.0. University of Colorado at Boulder

  61. Thaker DD, Impens F, Chuang IL, Amirtharajah R, Chong FT (2005) Recursive TMR: scaling fault tolerance in the nanoscale era. IEEE Des Test Comput 22(4): 298–305

    Article  Google Scholar 

  62. Trivedi KS (2002) SHARPE 2002: symbolic hierarchical automated reliability and performance evaluator. In: 2002 International conference on dependable systems and networks (DSN 2002), 23–26 June 2002, Bethesda, MD, USA, Proceedings, IEEE Computer Society, p 544

  63. Vesely WE, Goldberg FF, Roberts NH, Haasl DF (1981) Fault tree handbook. Technical report NUREG-0492, Systems and Reliability Research Office of Nuclear Regulatory Research. U.S. Nuclear Regulatory Commission

  64. Vesely WE, Stamatelatos M, Dugan J, Fragola J, Minarick III J, Railsback J (2002) Fault tree handbook with aerospace applications. Prepared for NASA Office of Safety and Mission Assurance, NASA Headquarters, Washington, DC

  65. Yeh YC (1996) Triple-triple redundant 777 primary flight computer. In: Aerospace applications conference, 1996. Proceedings, IEEE, vol 1, IEEE, pp 293–307

  66. Zhang M, Liu Z, Morisset C, Ravn AP (2009) Design and verification of fault-tolerant components. In: Butler MJ, Jones CB, Romanovsky A, Troubitsyna E (eds) Methods, models and tools for fault tolerance, vol 5454 of lecture notes in computer science, Springer, pp 57–84

Download references

Author information

Authors and Affiliations

  1. Fondazione Bruno Kessler, Trento, Italy

    Marco Bozzano & Alessandro Cimatti

  2. Stanford University, 353 Serra Mall, Stanford, CA, 94305, USA

    Cristian Mattarei

Authors
  1. Marco Bozzano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alessandro Cimatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cristian Mattarei
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cristian Mattarei.

Additional information

Anne Haxthausen

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bozzano, M., Cimatti, A. & Mattarei, C. Formal reliability analysis of redundancy architectures. Form Asp Comp 31, 59–94 (2019). https://doi.org/10.1007/s00165-018-0475-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-018-0475-1

Keywords

Search

Navigation