Slicing Behavior Tree Models for Verification

File Size Format
64589_1.pdf 235Kb Adobe PDF View
Title Slicing Behavior Tree Models for Verification
Author Yatapanage, Nisansala Prasanthi; Winter, Kirsten; Zafar, Saad
Publication Title Theoretical Computer Science
Editor Christian S.Calude and Vladimiro Sassone
Year Published 2010
Place of publication Germany
Publisher Springer
Abstract Program slicing is a reduction technique that removes irrelevant parts of a program automatically, based on dependencies. It is used in the context of documentation to improve the user's understanding as well as for reducing the size of a program when analysing. In this paper we describe an approach for slicing not program code but models of software or systems written in the graphical Behavior Tree language. Our focus is to utilise this reduction technique when model checking Behavior Tree models. Model checking as a fully automated analysis technique is restricted in the size of the model and slicing provides one means to improve on the inherent limitations. We present a Health Information System as a case study. The full model of the system could not be verified due to memory limits. However, our slicing algorithm renders the model to a size for which the model checker terminates. The results nicely demonstrate and quantify the benefits of our approach.
Peer Reviewed Yes
Published Yes
Alternative URI
Copyright Statement IFIP, 2010. This is the author's version of the work. It is posted here by permission of IFIP for your personal use. Not for redistribution. The definitive version was published in Theoretical Computer Science, IFIP AICT, Vol. 323, (Boston:Springer), pp.125-139.
ISBN 9783642152399
Conference name 6th IFIP International Conference on Theoretical Computer Science
Location Brisbane, Australia
Date From 2010-09-20
Date To 2010-09-23
Date Accessioned 2010-09-03
Language en_AU
Faculty Faculty of Science, Environment, Engineering and Technology
Subject Software Engineering
Publication Type Conference Publications (Full Written Paper - Refereed)
Publication Type Code e1

Show simple item record

Griffith University copyright notice