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
Artikel Terkait :
Jp Teknik Komputer gg 2013
- Gamelan Music Onset Detection based on Spectral Features
- Streamed Sampling on Dynamic data as Support for Classification Model
- A Mobile Ecotourism Recommendations System Using Cars-Context Aware Approaches
- Improved Harmony Search Algorithm with Chaos for Absolute Value Equation
- Future Smart Cooking Machine System Design
- A Review of Communication Protocols for Intelligent Remote Terminal Unit Development
- Power Balance AODV Algorithm of WSN in Agriculture Monitoring
- Circularly Polarized Proximity-Fed Microstrip Array Antenna for Micro Satellite
- Ovarian Cancer Identification using One-Pass Clustering and k-Nearest Neighbors
- Localizing Region-Based Level-set Contouring for Common Carotid Artery in Ultrasonography
- Separability Filter for Localizing Abnormal Pupil: Identification of Input Image
- Feature Extraction of Composite Damage on Acoustic Emission Signals
- A Camera Self-Calibration Method Based on Plane Lattice and Orthogonality
- Application of Wavelet Analysis in Detecting Runway Foreign Object Debris
- Palmprint Verification Using Time Series Method
- Time Series Based for Online Signature Verification
- Two-phase Flow Visualization Employing Gauss-Newton Method in Microchannel
- Study on Thermal Conductivity Methane Sensor Constant Temperature Detection Method
- Fuzzy Adaptive PID Control of a New Hydraulic Erecting Mechanism
- Optimization of Membership Functions for the Fuzzy Controllers of the Water Tank and Inverted Pendulum with Differents PSO Variants
- Study of an Improved Fuzzy Direct Torque Control of Induction Motor
- Research of NiMH Battery Modeling and Simulation Based on Linear Regression Analysis Method
- Design and Modeling of an Integrated Micro-Transformer in a Flyback Converter
- Renewable Distributed Generation Models in Three-Phase Load Flow Analysis for Smart Grid
- A Design Study of Dual-Stator Permanent Magnet Brushless DC Motor