Timed Behavior Trees and Their Application to Verifying Real-Time Systems
Timed Behavior Trees and Their Application to Verifying Real-Time Systems
复制标题
DOI：
10.1109/aswec.2007.49
复制
发表时间：
2007-04
期刊：
影响因子：
--
通讯作者：
Lars Grunske;Kirsten Winter;R. Colvin
中科院分区：
文献类型：
--
作者：
Lars Grunske;Kirsten Winter;R. Colvin
行为树(BTS)是一种用于形式化功能需求的图形符号，并已成功地应用于几个案例研究。然而，该符号目前不支持时间的概念，因此其应用仅限于非实时系统。为了克服这一限制，我们将该符号扩展到时间行为树，它可以由时间自动机在语义上定义。基于该扩展，我们能够在BT模型中包括本地时序假设，并且可以使用时序证明方法来验证系统级时序属性。我们通过案例研究验证了新符号的使用。为了验证系统级的时序特性，我们将模型转换为时间自动机，并使用UPPAAL工具进行时间模型检测。
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.