Irene Ully Havsa
Unknown Affiliation

Published : 1 Documents Claim Missing Document
Claim Missing Document
Check
Articles

Found 1 Documents
Search

UTILISING BTTRACE VISUALISER AND LTL FORMULAE PATTERNS FOR ANALYSING COUNTEREXAMPLE Irene Ully Havsa
Jurnal Ilmu Komputer dan Informasi Vol 6, No 1 (2013): Jurnal Ilmu Komputer dan Informasi (Journal of Computer Science and Information)
Publisher : Faculty of Computer Science - Universitas Indonesia

Show Abstract | Download Original | Original Source | Check in Google Scholar | Full PDF (590.716 KB) | DOI: 10.21609/jiki.v6i1.212

Abstract

The aim of this paper is to demonstrate the utilisation of a Behavior Tree trace visualiser called BTTrace and generalised LTL formulae patterns to help system analysts analyse counterexamples and generate valuable ones. Counterexample generated by SAL model checker from a Behavior Tree model and an LTL formulae is translated into a BTTrace file. This file is rendered by BTTrace to visualise the counterexample on Behavior Tree diagram in animated fashion. Generalised LTL formulae patterns are exploited using a particular technique to assist analyst on constructing new yet meaningful property formulas. These formulas are used to obtain different and valuable counterexamples for further analysis. It is shown that BTTrace and LTL formulae patterns give significant support for analysing counterexamples of Behavior Tree model.