Slicing Behavior Tree Models for Verification

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.
Type de document :
Communication dans un congrès
Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.125-139, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_10〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01054464
Contributeur : Hal Ifip <>
Soumis le : mercredi 6 août 2014 - 16:26:17
Dernière modification le : mardi 16 janvier 2018 - 17:56:01
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 01:01:46

Fichier

03230126.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Nisansala Yatapanage, Kirsten Winter, Saad Zafar. Slicing Behavior Tree Models for Verification. Cristian S. Calude; Vladimiro Sassone. 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS) / Held as Part of World Computer Congress (WCC), Sep 2010, Brisbane, Australia. Springer, IFIP Advances in Information and Communication Technology, AICT-323, pp.125-139, 2010, Theoretical Computer Science. 〈10.1007/978-3-642-15240-5_10〉. 〈hal-01054464〉

Partager

Métriques

Consultations de la notice

163

Téléchargements de fichiers

127