UTILISING BTTRACE VISUALISER AND LTL FORMULAE PATTERNS FOR ANALYSING COUNTEREXAMPLE
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.
Author: Irene Ully Havsa
Journal Code: jptkomputergg130006
