×

zbMATH — the first resource for mathematics

Model based importance analysis for minimal cut sets. (English) Zbl 1183.68365
Cha, Sungdeok (Steve) (ed.) et al., Automated technology for verification and analysis. 6th international symposium, ATVA 2008, Seoul, Korea, October 20–23, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-88386-9/pbk). Lecture Notes in Computer Science 5311, 303-317 (2008).
Summary: We show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Based on standard design notations (Statecharts) annotated with fault occurrence distributions we compute to what extent certain fault configurations contribute to the probability of reaching a safety-critical state.
For the entire collection see [Zbl 1148.68001].
Reviewer: Reviewer (Berlin)
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
90B20 Traffic problems in operations research
90B25 Reliability, availability, maintenance, inspection in operations research
Software:
MRMC; SIGREF
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Åkerlund, O., et al.: ISAAC, a framework for integrated safety analyses of functional, geometrical and human aspects. ERTS (2006)
[2] Vesely, W.E., Dugan, J., Fragola, J., Minarick III, J., Railsback, J.: Fault Tree Handbook with Aerospace Applications. National Aeronatics and Space Administration (August 2002)
[3] Peikenkamp, T., Cavallo, A., Valacca, L., Böde, E., Pretzer, M., Hahn, E.M.: Towards a unified model-based safety assessment. In: Górski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 275–288. Springer, Heidelberg (2006) · doi:10.1007/11875567_21
[4] Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional performability evaluation for statemate. In: 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006, Riverside (USA), pp. 167–178. IEEE Computer Society Press, Los Alamitos (2006)
[5] Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional performability evaluation for statemate. In: Quantitative Evaluation of Computer Systems - Special issue of IEEE Transactions on Software Engineering (to appear, 2008)
[6] Harel, D., Politi, M.: Modelling Reactive Systems with Statecharts: The STATEMATE Approach. McGraw-Hill, New York (1998)
[7] Hermanns, H., Katoen, J.P.: Automated compositional markov chain generation for a plain-old telephone system. Science of Computer Programming 36(1), 97–127 (2000) · Zbl 0941.68649 · doi:10.1016/S0167-6423(99)00019-2
[8] Pulungan, R., Hermanns, H.: Orthogonal distance fitting for phase-type distributions. Reports of SFB/TR 14 AVACS 10, SFB/TR 14 AVACS (November 2006) ISSN: 1860-9821, http://www.avacs.org
[9] Hermanns, H.: Interactive Markov Chains – The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002) · Zbl 1012.68142 · doi:10.1007/3-540-45804-2
[10] Hermanns, H., Johr, S.: Uniformity by construction in the analysis of nondeterministic stochastic systems. In: International Conference on Dependable Systems and Networks, DSN 2007 (2007) · doi:10.1109/DSN.2007.96
[11] Boudali, H., Crouzen, P., Stoelinga, M.: Dynamic fault tree analysis using input/output interactive markov chains. In: DSN 2007: Proceedings of the 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, Washington, DC, USA, pp. 708–717. IEEE Computer Society Press, Los Alamitos (2007) · Zbl 1141.68454
[12] Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996) · doi:10.1145/235321.235322
[13] Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980) · Zbl 0452.68027 · doi:10.1007/3-540-10235-3
[14] Glabbeek, R., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996) · Zbl 0882.68085 · doi:10.1145/233551.233556
[15] Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref – a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477–492. Springer, Heidelberg (2006) · Zbl 1161.68631 · doi:10.1007/11901914_35
[16] Hermanns, H., Johr, S.: May we reach it? or must we? in what time? with what probability? In: Proceedings 14th GI/ITG Conference on Measuring, Modelling and Evaluation of Computer and Communication Systems (MMB 2008), Dortmund, Germany, March 31 - April 2, 2008, VDE Verlag (to appear, 2008)
[17] Johr, S.: Model Checking Compositional Markov Systems. PhD thesis, Universität des Saarlandes, Saarbrücken (2007) · Zbl 1144.68040
[18] Katoen, J.P., Khattri, M., Zapreev, I.S.: A markov reward model checker. In: Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005), Torino, Italy, 19-22 September 2005, pp. 243–244. IEEE Computer Society Press, Los Alamitos (2005) · doi:10.1109/QEST.2005.2
[19] ERTMS User Group, UNISIG: ETCS Application Level 2 - Safety Analysis - Part 1 - Functional Fault Tree. Technical report, ALCATEL,ALSTOM,ANSALDO SIGNAL,BOMBARDIER,INVENSYS RAIL,SIEMENS
[20] Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. European Assoc. for Software Science and Technology (EASST) Newsletter 4, 13–24 (2002)
[21] BCG_MIN: Project Website (March 2006), http://www.inrialpes.fr/vasy/cadp/man/bcg_min.html
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.