Abstract
Formal risk analysis (FRA) is a means for automatic generation of fault trees for failures of sensors, actuators, and other input and output devices. FRA can be used to automate significant parts of the manual fault tree analysis work, and hence automate the proof of fail-safe behavior. Because FRA is based on information that is already used for formal verification, no additional effort is necessary for the automatic generation of fault trees with FRA. While formal verification focuses on the functional aspects, in particular safety functions, the fault tree analysis with FRA focuses on the system integrity. FRA significantly reduces the effort for the generation of fault trees. This paper describes Formal Risk Analysis and its application for the proof of fail-safe behavior.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Akers S. B. Binary Decision Diagrams, IEEE Trans. Comp. Vol. C-27, No. 6, June 1978, pp. 509–516
Allen D. J. Digraphs and Fault Trees, Hazard Prevention January/February 1983, pp. 22–25
Bader P., Päppinghaus P., Pichler C., Schmid R., Umbreit G., Winkelmann K. CSL Referenzmanual — Sprachbeschreibung, Internal Report, Siemens AG, München, 1996
Bollig B., Wegener I. Improving the Variable Ordering of OBDDs is NP-Complete, IEEE Trans. Comp., Vol. 45, No. 9, September 1996, pp. 993–1001
Bormann J., Lohse J., Payer M., Venzl G. Model Checking in Industrial Hardware Design, 32nd ACM/IEEE Design Automation Conference 1995
Bryant R. E. Graph-Based Algorithms for Boolean Function Manipulation, IEEE Trans. Comp., Vol. C-35, No.8, August 1986, pp. 667–691
Bryant R. E. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams, ACM Computing Surveys, Vol. 24, No.3, September 1992, pp. 293–318
Burch J. R., Clarke E. M., Long D. E., McMillan K. L., Dill D. L. Symbolic Model Checking for Sequential Circuit Verification, IEEE Design & Test, Vol. 13 No. 4, April 1994, pp. 401–424
Campos S., Clarke E., Marrero W., Minea M. Timing analysis of industrial real-time systems, In: Workshop on Industrial Strength Formal Specification Techniques, 1995.
Filkorn T., Schneider H.-A., Scholz A., Strasser A., Warkentin P. SVE Users’ Guide, Internal Report, Siemens AG, München, 1996
Lee C. Y. Representation of Switching Circuits by Binary-Decision Programs, The Bell System Technical Journal 38, July 1959, pp. 985–999
Lewerentz C., Lindner T. Formal Development of Reactive Systems: Case Study Production Cell, LNCS 891, Springer-Verlag, January 1995
Liggesmeyer P., Rothfelder M. Improving System Reliability with Automatic Fault Tree Generation, Proc. FTCS-28, Munich, Germany, 1998, pp. 90–99
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg Berlin Heidelberg
About this paper
Cite this paper
Liggesmeyer, P., Rothfelder, M. (1998). Towards Automated Proof of Fail-Safe Behavior. In: Ehrenberger, W. (eds) Computer Safety, Reliability and Security. SAFECOMP 1998. Lecture Notes in Computer Science, vol 1516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49646-7_13
Download citation
DOI: https://doi.org/10.1007/3-540-49646-7_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65110-9
Online ISBN: 978-3-540-49646-5
eBook Packages: Springer Book Archive