Timed behavior trees and their application to verifying real-time systems

Behavior Trees (BTs) are a graphical notation used for formalising functional requirements and have been successfully applied to several case studies. However, the notation currently 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, which can be semantically defined by timed automata. Based on this extension we are able to include local timing assumptions in a BT model and can verify system-level timing properties with temporal proof methodologies. We validate the use of the new notation by means of a case study. To verify system-level timing properties we translate the model into timed automata and use the tool UPPAAL for timed model checking.