Timed Behavior Trees for Failure Mode and Effects Analysis of time-critical systems

Behavior Trees are a graphical notation used for formalising functional requirements, and have been successfully applied to several industrial case studies. However, the standard notation does not support the concept of time, and consequently its application is limited to non-real-time systems. To overcome this limitation we extend the notation to timed Behavior Trees. We provide an operational semantics which is based on timed automata, and thus serves as a formal basis for the translation of timed Behavior Trees into the input notation of the timed model checker UPPAAL. System-level timing properties of a Behavior Tree model can then be automatically verified using UPPAAL. Based on the notational extensions with model checking support, we introduce timed Failure Mode and Effects Analysis, a process for identifying cause-consequence relationships between component failures and system hazards in real-time safety critical systems.