loading...
Timed Behavior Trees and Their Application to Verifying Real-Time Systems
Melbourne, Australia April 10-April 13
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASWEC.2007.492007 Australian Software Engineering ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Lars Grunske, University of Queensland, Australia
Kirsten Winter, University of Queensland, Australia
Robert Colvin, University of Queensland, Australia
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.
Index Terms:
Behavior Trees, real time systems, timed automata, model checking, requirements engineering
Citation:
Lars Grunske, Kirsten Winter, Robert Colvin, "Timed Behavior Trees and Their Application to Verifying Real-Time Systems," aswec, pp.211-222, 2007 Australian Software Engineering Conference (ASWEC'07), 2007
Usage of this product signifies your acceptance of the Terms of Use.