Guided Search Technique for LOTOS

Mazen Haj-Hussein
PhD Thesis

University of Ottawa
1995

Abstract

The dynamic behaviour of a LOTOS specification can be described as a tree,
called behaviour tree, where the nodes represent the states of the
behaviour, and the branches represent the possible next actions.
Unfortunately, the behaviour tree for a realistic size LOTOS specification
can be very large and often has no finite representation.This is the major
limitation for the existing LOTOS verification techniques.

The main goal of this thesis is to provide a new behaviour tree
exploration technique, called Goal-Oriented Execution, that can be used to
check properties of LOTOS specifications by narrowing exploration to a
meaningfully selected subset of the tree. In this execution technique, the
system derives traces (i.e paths in the behaviour tree) satisfying certain
assertions that express temporal ordering of actions and data values
properties.

Goal-Oriented Execution is a combination of three techniques. The first
technique is an automatically generated ADT evaluator/narrower engine. It
is capable of evaluating an expression based on a rewriting rule approach,
borrowed from functional programming, and deriving solutions to a set of
constraints using a narrowing technique, borrowed from logic programming.
The second technique is a static analyzer that determines where the given
assertions are likely to hold, producing static information called static
derivation paths. The third technique, called guided- inference system,
involves a new type of inference rules that derive traces using static
derivation paths to resolve most non-determinism.

Implementation issues of this technique are also discussed, and examples
of its usage are provided. The technique is now included in ELUDO, the
University of Ottawa LOTOS interpreter.