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

Grunske, Lars, Winter, Kirsten and Colvin, Robert (2007). Timed behavior trees and their application to verifying real-time systems. In: J. Grundy and J. Han, Proceedings of the 2007 Australian Conference on Software Engineering. Australian Conference on Software Engineering (ASWEC 2007), Melbourne, Australia, (211-222). 10-13 April 2007. doi:10.1109/ASWEC.2007.49

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

Author Grunske, Lars
Winter, Kirsten
Colvin, Robert
Title of paper Timed behavior trees and their application to verifying real-time systems
Conference name Australian Conference on Software Engineering (ASWEC 2007)
Conference location Melbourne, Australia
Conference dates 10-13 April 2007
Convener Australian Computer Society
Proceedings title Proceedings of the 2007 Australian Conference on Software Engineering
Journal name 2007 Australian Software Engineering Conference, Proceedings
Place of Publication Washington, DC, USA
Publisher IEEE Computer Society
Publication Year 2007
Sub-type Fully published paper
DOI 10.1109/ASWEC.2007.49
ISBN 0769527787
9780769527789
ISSN 1530-0803
Editor J. Grundy
J. Han
Start page 211
End page 222
Total pages 12
Collection year 2008
Language eng
Abstract/Summary 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.
Subjects 280302 Software Engineering
700102 Application tools and system utilities
E1
Keyword Behavior Trees
Real time systems
Timed automata
Model checking
Requirements engineering
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 12 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 18 Apr 2008, 17:38:40 EST by Donna Clark on behalf of School of Information Technol and Elec Engineering