Abstract
Safety is increasingly important for software based, critical systems. Fault tree analysis (FTA) is a safety technique from engineering, developed for analyzing and assessing system safety by uncovering safety flaws and weaknesses of the system. The main drawback of this analysis technique is, that it is based on informal grounds, so safety flaws may be overlooked. This is an issue, where formal proofs can help. They are a safety techniques from software engineering, which are based on precise system descriptions and allow to prove consistency and other (safety) properties.
We present an approach which automatically proves the consistency of fault trees based on a formal model by model checking. Therefore, we define consistency conditions in Computational Tree Logic, a widely used input language for model checkers. In the second part, we exemplify our approach with a case study from the Fault Tree Handbook.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 363. Springer, Heidelberg (2000)
Bruns, G., Anderson, S.: Validating safety models with fault trees. In: Górski, J. (ed.) SafeComp 1993: 12th International Conference on Computer Safety, Reliability, and Security, pp. 21–30. Springer, Heidelberg (1993)
Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)
Filkorn, T., Schneider, H.A., Scholz, A., Strasser, A., Warkentin, P.: SVE user’s guide. Technical Report ZFE BT SE 1-SVE-1, Siemens AG, Corporate Research and Development, Munich (1994)
Góski, J.: Extending safety analysis techniques with formal semantics. In: Redmill, F.J., Anderson, T. (eds.) Technology and Assessment of Safety Critical Systems, pp. 147–163. Springer, London (1994)
Hansen, K.M., Ravn, A.P., Stavridou, V.: From safety analysis to formal specification. ProCoS II document [ID/DTH KMH 1/1], Technical University of Denmark (1994)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 17(3), 333–354 (1983)
Leveson, N.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1990)
Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2), 10–19 (1985)
Pandya, P.K.: Model checking CTL∗[DC]. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 559. Springer, Heidelberg (2001)
Pandya, P.K.: Specifying and deciding qauntified discrete-time duration calculus formulae using DCVALID. In: Proceedings of Workshop on Real-Time Tools RTTOOL 2001, Aalborg, Denmark (August 2001)
Ruf, J.: RAVEN: Real-time analyzing and verification environment. Technical Report WSI 2000-3, University of Tübingen, Wilhelm-Schickard-Institute (January 2000)
Ruf, J., Kropf, T.: Modeling real-time systems with I/O-interval structures. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen ud Systemen. Shaker Verlag, Aachen (1999)
Ruf, J., Kropf, T.: Modeling real-time systems with I/O-interval structures. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, March 1999, pp. 91–100. Shaker Verlag, Aachen (1999)
Ruf, J., Kropf, T.: Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals. In: Cerny, E., Probst, D.K. (eds.) Conference on Correct Hardware Design and Verification Methods (CHARME), Montreal. IFIP WG 10.5, pp. 146–166. Chapman and Hall, Boca Raton (1997)
Ruf, J., Kropf, T.: Using MTBDDs for Composition and Model Checking of Real-Time Systems. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 185–202. Springer, Heidelberg (1998)
Schäfer, A.: Fehlerbaumanalyse und Model-Checking. Master’s thesis, Universität Oldenburg (2001) (in German)
Schellhorn, G., Thums, A., Reif, W.: Formal fault tree semantics. In: Proceedings of The Sixth World Conference on Integrated Design & Process Technology, Pasadena, CA (2002)
Tapken, J.: Model-checking of duration calculus specifications. Master’s thesis, University of Oldenburg (June 2001), http://semantik.informatik.uni-oldenburg.de/projects/
Thums, A., Schellhorn, G., Reif, W.: Comparing fault tree semantics. In: Haneberg, D., Schellhorn, G., Reif, W. (eds.) FM-TOOLS 2002, Technical Report 2002-11, pp. 25–32. Universität Augsburg (2002)
Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook, Washington, D.C. (1981) NUREG-0492
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thums, A., Schellhorn, G. (2003). Model Checking FTA. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_40
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive