Abstract
Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Lutz, R.R.: Software engineering for safety: a roadmap. In: ICSE - Future of SE Track, pp. 213–226 (2000)
Neumann, P.G.: Computer-Related Risks. ACM Press / Addison Wesley (1995)
Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Reading (1995)
Department of Defence: MIL-STD-1629A, Procedures for Performing a Failure Mode, Effects and Criticality Analysis. Washington (1980)
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Heitmeyer, C., Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering 24, 927–947 (1998)
Atlee, J., Gannon, J.: State-based model checking of event-driven system requirements. IEEE Transactions on Software Engineering 19, 24–40 (1993)
Tiwari, A., Shankar, N., Rushby, J.: Invisible formal methods for embedded control systems. Proceedings of the IEEE 91, 29–39 (2003)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Coomputer Science, vol. B. Elsevier Science Publishers, Amsterdam (1990)
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)
Back, R.J., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)
Dromey, R.G.: From requirements to design: Formalizing the key steps. In: Int. Conference on Software Engineering and Formal Methods (SEFM 2003), pp. 2–13. IEEE Computer Society Press, Los Alamitos (2003)
Wen, L., Dromey, R.G.: From requirements change to design change: A formal path. In: Int. Conference on Software Engineering and Formal Methods (SEFM 2004), pp. 104–113. IEEE Computer Society Press, Los Alamitos (2004)
GSE: Genetic Software Engineering (2005), http://www.sqi.gu.edu.au/gse
Bitsch, F.: Safety patterns - the key to formal specification of safety requirements. In: Voges, U. (ed.) SAFECOMP 2001. LNCS, vol. 2187, pp. 176–189. Springer, Heidelberg (2001)
Atchison, B., Lindsay, P., Tombs, D.: A case study in software safety assurance using formal methods. Technical report, University of Queensland, SVRC 99-31 (1999), http://www.itee.uq.edu.au/~pal/SVRC/tr99-31.pdf
McDermid, J., Kelly, T.: Industrial press: Safety case. Technical report, High Integrity Systems Engineering Group, University of York (1996)
Smith, C., Winter, K., Hayes, I., Dromey, G., Lindsay, P., Carrington, D.: An environment for building a system out of its requirements. In: Int. Conference on Automated Software Engineering (ASE 2004), pp. 398–399. IEEE Computer Society Press, Los Alamitos (2004)
Abdulla, P.A., Deneux, J., Akerlund, O.: Designing safe, reliable systems using Scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115–129. Springer, Heidelberg (2006)
Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49–62. Springer, Heidelberg (2003)
Papadopoulos, Y., Parker, D., Grante, C.: Automating the failure modes and effects analysis of safety critical systems. In: Int. Symposium on High-Assurance Systems Engineering (HASE 2004), pp. 310–311. IEEE Computer Society Press, Los Alamitos (2004)
Papadopoulos, Y., McDermid, J.A., Sasse, R., Heiner, G.: Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Int. Journal of Reliability Engineering and System Safety 71, 229–247 (2001)
Rae, A., Lindsay, P.: A behaviour-based method for fault tree generation. In: Int. System Safety Conference, System Safety Society, pp. 289–298 (2004)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)
Cleaveland, R., Sims, S.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394–397. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grunske, L., Lindsay, P., Yatapanage, N., Winter, K. (2005). An Automated Failure Mode and Effect Analysis Based on High-Level Design Specification with Behavior Trees. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_9
Download citation
DOI: https://doi.org/10.1007/11589976_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)