×

The mechanical generation of fault trees for reactive systems via retrenchment. I. Combinational circuits. (English) Zbl 1298.68050


MSC:

68M15 Reliability, testing and fault tolerance of networks and computer systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
94C12 Fault detection; testing in circuits and networks
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Galileo
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aldemir T (1987) Computer-assisted Markov failure modeling of process control systems. IEEE Trans Reliab R36:133-144 · Zbl 0621.90034 · doi:10.1109/TR.1987.5222318
[2] Anand A, Somani AK (1998) Hierarchical analysis of fault trees with dependencies, using decomposition. In: Proceedings of annual reliability and maintainability symposium, pp 69-75
[3] Bozzano M et al (2006) ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proceedings of European congress on embedded real time software (ERTS 2006)
[4] Banach R, Bozzano M (2010) The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits. doi:10.1007/s00165-011-0203-6 · Zbl 1298.68051
[5] Banach, R.; Cross, R.; Heisel, M. (ed.); Liggesmeyer, P. (ed.); Wittmann, S. (ed.), Safety requirements and fault trees using retrenchment, 210-223 (2004), Potsdam, Germany · doi:10.1007/978-3-540-30138-7_18
[6] Bozzano M, Cavallo A, Cifaldi M, Valacca L, Villafiorita A (2003) Improving safety assessment of complex systems: an industrial case study. In: International symposium of formal methods Europe (FME 2003), Pisa, Italy. LNCS, vol 2805, pp 208-222
[7] Bozzano M, Cimatti A, Tapparo F (2007) Symbolic fault tree analysis for reactive systems. In: Proceedings of symposium on automated technology for verification and analysis (ATVA 2007), pp 162-176 · Zbl 1141.68455
[8] Banach R, Jeske C (2009) Retrenchment and refinement interworking: the tower theorems. Submitted. See [Ret] · Zbl 1361.68056
[9] Banach R, Jeske C, Poppleton M (2008) Composition mechanisms for retrenchment. J Log Alg Prog 75:209-229 · Zbl 1137.68037 · doi:10.1016/j.jlap.2007.11.001
[10] Banach R, Poppleton M (1998) Retrenchment: an engineering variation on refinement. In: B’98: Recent advances in the development and use of the B method. Second international B conference, Montpellier, France. LNCS, vol 1393, pp 129-147
[11] Banach R, Poppleton M (2003) Retrenching partial requirements into system definitions: a simple feature interaction case study. Requir Eng J 8:266-288 · doi:10.1007/s00766-002-0157-6
[12] Banach, R.; Poppleton, M.; Jeske, C.; Stepney, S.; Fitzgerald, J. (ed.); Hayes, I. (ed.); Tarlecki, A. (ed.), Retrenching the purse: finite sequence numbers and the tower pattern, 382-398 (2005), Newcastle, UK · Zbl 1120.68406 · doi:10.1007/11526841_26
[13] Banach R, Jeske C, Poppleton M, Stepney S (2006) Retrenching the Purse: finite exception logs, and validating the small. In: Hinchey M (ed) Proc. IEEE/NASA SEW30-06, pp 234-245 · Zbl 1120.68406
[14] Banach R, Jeske C, Poppleton M, Stepney S (2006) Retrenching the purse: hashing injective CLEAR codes, and security properties. In: Margaria T, Steffen B (eds) Proc. IEEE ISOLA-06, pp 82-90 · Zbl 0825.68162
[15] Banach R, Poppleton M, Jeske C, Stepney S (2007) Engineering and theoretical underpinnings of retrenchment. Sci Comp Prog 67:301-329 · Zbl 1119.68348 · doi:10.1016/j.scico.2007.04.002
[16] Bryant RE (1992) Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Comput Surv 24(3):293-318 · doi:10.1145/136035.136043
[17] Bozzano M, Villafiorita A (2003) Integrating fault tree analysis with event ordering information. In: Proceedings of ESREL 2003, pp 247-254 · Zbl 1120.68406
[18] Bozzano M, Villafiorita A et al (2003) ESACS: an integrated methodology for design and safety analysis of complex systems. Proceedings of 2003, pp 237-245
[19] Bozzano M, Villafiorita A (2007) The FSAP/NuSMV-SA safety analysis platform. Int J Softw Tools Technol Transf 9(1):5-24 · doi:10.1007/s10009-006-0001-2
[20] Cojazzi G, Izquierdo JM, Meléndez E, Perea MS (1992) The reliability and safety assessment of protection systems by the use of dynamic event trees. The DYLAM-TRETA Package. In: Proceedings of XVIII Annual Meeting Spanish Nucl Soc · Zbl 0621.90034
[21] Coudert O, Madre JC (1992) Implicit and incremental computation of primes and essential primes of Boolean functions. In: Proceedings of design automation conference (DAC 1992), pp 36-39. IEEE Computer Society Press · Zbl 1137.68037
[22] Coudert O, Madre JC (1993) Fault tree analysis: 1020 prime implicants and beyond. In: Proceedings of annual reliability and maintainability symposium (RAMS 1993)
[23] Dugan J, Bavuso S, Boyd M (1992) Dynamic fault tree models for fault tolerant computer systems. IEEE Trans Reliab 41(3):363-377 · Zbl 0825.68162 · doi:10.1109/24.159800
[24] Dutuit Y, Rauzy A (1996) A linear-time algorithm to find modules in fault trees. IEEE Trans Reliab 45(3):422-425 · doi:10.1109/24.537011
[25] de Roever WP, Engelhardt K (1998) Data refinement model-oriented proof methods and their comparison. Cambridge University Press · Zbl 0955.68076
[26] Fenelon P, McDermid JA, Nicholson M, Pumfrey DJ (1994) Towards integrated safety analysis and design. Appl Comput Rev 2(1):21-32 · doi:10.1145/381766.381770
[27] The FSAP/NuSMV-SA platform. http://sra.itc.it/tools/FSAP. Accessed 13 Sep 2011
[28] SAE International. Guidelines and methods for conducting the safety assessment process on civil airborne systems and equipment, December 1996
[29] Isograph. http://www.isograph-software.com. Accessed 13 Sep 2011
[30] Jeske C (2005) Algebraic integration of retrenchment and refinement. PhD thesis, University of Manchester
[31] Joshi A, Heimdahl MPE (2005) Model-based safety analysis of Simulink models using SCADE Design Verifier. In: Winther R, Gran BA, Dahll G (eds) Proceedings of conference on computer safety, reliability and security (SAFECOMP 2005). LNCS, vol 3688, pp 122-135. Springer
[32] Joshi A, Miller SP, Whalen M, Heimdahl MPE (2005) A proposal for model-based safety analysis. In: Proceedings of AIAA/IEEE digital avionics systems conference (DASC 2005)
[33] Manian R, Dugan JB, Coppit D, Sullivan KJ (1998) Combining various solution techniques for dynamic fault tree analysis of computer systems. In: Proceedings of high-assurance systems engineering symposium (HASE 1998), pp 21-28. IEEE
[34] Manquinho VM, Oliveira AL, Marques-Silva JP (1998) Models and algorithms for computing minimum-size prime implicants. In: Proceedings of international workshop on Boolean problems (IWBP 1998)
[35] Miller SP, Tribble AC, Heimdahl MPE (2003) Proving the Shalls. In: Proceedings of formal methods Europe (FM 2003). LNCS, vol 2805, pp 75-93. Springer
[36] Marseguerra M, Zio E, Devooght J, Labeau PE (1998) A concept paper on dynamic reliability via Monte Carlo simulation. Math Comput Simul 47:371-382 · doi:10.1016/S0378-4754(98)00112-8
[37] Papazoglou IA (1994) Markovian reliability analysis of dynamic systems. In: Aldemir T, Siu NO, Mosleh A, Cacciabue PC, Göktepe BG (eds) Reliability and safety assessment of dynamic process systems. NATO ASI Series F, vol 120, pp 24-43. Springer
[38] Papadopoulos Y (2000) Safety-directed system monitoring using safety cases. PhD thesis, Department of Computer Science, University of York. Technical report YCST-2000-08
[39] Papadopoulos Y, Maruhn M (2001) Model-based synthesis of fault trees from Matlab-Simulink models. In: Proceedings of conference on dependable systems and networks (DSN 2001), pp 77-82
[40] Papadopoulos Y, McDermid J, Sasse R, Heiner G (2001) Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Reliab Eng Syst Saf 71(3):229-247 · doi:10.1016/S0951-8320(00)00076-4
[41] 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
[42] Rauzy A, Dutuit Y (1997) Exact and truncated computations of prime implicants of coherent and non-coherent fault trees within Aralia. Reliab Eng Syst Saf 58(2):127-144 · doi:10.1016/S0951-8320(97)00034-3
[43] Retrenchment Homepage. http://www.cs.man.ac.uk/retrenchment. Accessed 13 Sep 2011
[44] Remenyte-Prescott R, Andrews JD (2008) An enhanced component connection method for conversion of fault trees to binary decision diagrams. Reliab Eng Syst Saf 93(10):1543-1550 · doi:10.1016/j.ress.2007.09.001
[45] Schäfer A (2003) Combining real-time model-checking and fault tree analysis. In: Proceedings of formal methods Europe (FM 2003). LNCS, vol 2805, pp 522-541. Springer
[46] Smidts C, Devooght J (1992) Probabilistic reactor dynamics II. A Monte-Carlo study of a fast reactor transient. Nucl Sci Eng 111(3):241-256
[47] Sullivan KJ, Dugan JB, Coppit D (1999) The Galileo fault tree analysis tool. In: Proceedings of symposium on fault-tolerant computing (FTCS 1999), pp 232-235. IEEE
[48] Siu NO (1994) Risk assessment for dynamic systems: an overview. Reliab Eng Syst Saf 43:43-74 · doi:10.1016/0951-8320(94)90095-7
[49] Tribble AC, Lempia DL, Miller SP (2002) Software safety analysis of a flight guidance system. In: Proceedings of AIAA/IEEE digital avionics systems conference (DASC 2002)
[50] Tribble AC, Miller SP (2003) Software safety analysis of a flight management system vertical navigation function—a status report. In: Proceedings of AIAA/IEEE digital avionics systems conference (DASC 2003)
[51] Thums A, Schellhorn G (2003) Model checking FTA. In: Proceedings of formal methods Europe (FM 2003). LNCS, vol 2805, pp 739-757. Springer
[52] 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
[53] Vesely WE, Stamatelatos M, Dugan J, Fragola J, Minarick III J, Railsback J (2002) Fault tree handbook with aerospace applications. Technical report, NASA
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.