| [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 · Zbl 0697.68010 |
| [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 · Zbl 0279.94024 · doi:10.1109/T-C.1974.224016 |
| [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 · Zbl 1109.68101 · doi:10.1007/s10817-005-9004-z |
| [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 · Zbl 1165.68482 |
| [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 · doi:10.1093/comjnl/bxq024 |
| [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 · doi:10.1016/j.ress.2014.07.003 |
| [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 · Zbl 1141.68455 |
| [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 · doi:10.2514/1.26311 |
| [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 · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819 |
| [17] |
Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3): 293-318 · doi:10.1145/136035.136043 |
| [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 · Zbl 1183.68568 |
| [20] |
Bozzano M, Villafiorita A (2007) The FSAP/NuSMV-SA safety analysis platform. STTT 9(1): 5-24 · doi:10.1007/s10009-006-0001-2 |
| [21] |
Bozzano M, Villafiorita A (2010) Design and safety assessment of critical systems: an Auerbach book. CRC Press, Boca Raton · doi:10.1201/b10094 |
| [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.; Čepin, M. (ed.), Reliability block diagram, 119-123 (2011), Berlin |
| [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 · Zbl 1381.68153 |
| [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 · doi:10.1016/S0951-8320(01)00024-2 |
| [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 · Zbl 1144.68371 |
| [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 · doi:10.1109/TR.2004.833308 |
| [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 · doi:10.1109/32.588521 |
| [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 · Zbl 1126.68015 |
| [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 · doi:10.1587/elex.4.657 |
| [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 · Zbl 1103.68628 |
| [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 · Zbl 1353.68055 |
| [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 · Zbl 1132.68474 |
| [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 · doi:10.1016/0951-8320(93)90060-C |
| [57] |
Rauzy A (2001) Mathematical foundations of minimal cutsets. IEEE Trans Reliab 50(4): 389-396 · doi:10.1109/24.983400 |
| [58] |
Sanders William H, Obal WD II, Qureshi MA, Widjanarko FK (1995) The UltraSAN modeling environment. Perform Eval 24(1-2): 89-115 · Zbl 0875.68664 · doi:10.1016/0166-5316(95)00012-M |
| [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 · Zbl 1183.68568 |
| [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 · doi:10.1109/MDT.2005.93 |
| [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 · Zbl 1234.68040 |
