Safety assessment using behavior trees and model checking

Lindsay, Peter A., Winter, Kirsten and Yatapanage, Nisansala (2010). Safety assessment using behavior trees and model checking. In: 2010 8th IEEE International Conference on Software Engineering and Formal Methods. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, (181-190). 13-18 September 2010. doi:10.1109/SEFM.2010.23

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Lindsay, Peter A.
Winter, Kirsten
Yatapanage, Nisansala
Title of paper Safety assessment using behavior trees and model checking
Conference name Software Engineering and Formal Methods (SEFM 2010)
Conference location Pisa, Italy
Conference dates 13-18 September 2010
Proceedings title 2010 8th IEEE International Conference on Software Engineering and Formal Methods
Journal name Proceedings - Software Engineering and Formal Methods, SEFM 2010
Place of Publication Piscataway, NJ, United States
Publisher IEEE Computer Society Press
Publication Year 2010
Sub-type Fully published paper
DOI 10.1109/SEFM.2010.23
Open Access Status
ISBN 9780769541532
Issue Article number 5637427
Start page 181
End page 190
Total pages 10
Collection year 2011
Language eng
Abstract/Summary This paper demonstrates the use of Behavior Trees and model checking to assess system safety requirements for a system containing substantial redundancy. The case study concerns the hydraulics systems for the Airbus A320 aircraft, which are critical for aircraft control. The system design is supposed to be able to handle up to 3 different components failing individually, without loss of all hydraulic power. Verifying the logic of such designs is difficult for humans because of the sheer amount of detail and number of different cases that need to be considered. The paper demonstrates how model checking can yield insights into what combinations of component failures can lead to system failure.
Keyword Automated failure analysis
Behavior trees
Cutset analysis
Formal modelling
Model checking
Safety requirements
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Session 5: Applications of Formal Methods Article number 5637427

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 4 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 09 Feb 2011, 11:34:40 EST by Dr Kirsten Winter on behalf of School of Information Technol and Elec Engineering