An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Grunske, Lars, Lindsay, Peter, Yatapanage, Nisansala and Winter, Kirsten (2005). An automated failure mode and effect analysis based on high-level design specificication with behavior trees. In: , Integrated Formal Methods: 5th International Conference. Integrated Formal Methods 2005, Eindhoven, The Netherlands, (129-149). 29 November - 2 December 2005.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
Author Grunske, Lars
Lindsay, Peter
Yatapanage, Nisansala
Winter, Kirsten
Title of paper An automated failure mode and effect analysis based on high-level design specificication with behavior trees
Conference Paper Type Fully Published Paper
Conference name Integrated Formal Methods 2005    (ERA 2010 Rank B)
Conference location Eindhoven, The Netherlands
Conference dates 29 November - 2 December 2005
Proceedings title Integrated Formal Methods: 5th International Conference
Place published Heidelberg, Germany
Publisher Springer
Publication date 2005
Volume number 3771
ISBN 3540304924
Start page 129
End page 149
Total pages 21
Collection year 2005
Language eng
Abstract/Summary 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.
Subjects 080309 Software Engineering
080399 Computer Software not elsewhere classified
Keyword Computer Science, Theory & Methods
Automated Hazard Analysis
Fmea
High-level Design Specification
Model Checking
Behavior Trees
Sal
Systems
Requirements
Checking
Q-Index Code E1
Q-Index Status Provisional Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 15 times in Thomson Reuters Web of Science Article | Citations
Google Scholar Search Google Scholar
Access Statistics: 102 Abstract Views, 5 File Downloads  -  Detailed Statistics
Created: Thu, 23 Aug 2007, 21:09:24 EST