Guided search technique for LOTOS.

• Main Author: Haj-Hussein, Mazen.
• Other Authors: Logrippo, Luigi
• Format: Others
• Published: University of Ottawa (Canada) 2009
• Subjects: Computer Science.
• Online Access: http://hdl.handle.net/10393/10085; http://dx.doi.org/10.20381/ruor-16648

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.