GOAL-ORIENTED EXECUTION FOR LOTOS

The dynamic semantics of LOTOS are defined in terms of axioms and inference rules which generate, from a given behaviour expression, the next possible actions and their resulting behaviour expressions. In this paper, we present a new type of inference rules, which are capable of generating traces of actions leading to a pre-selected action in the specification. These inference rules are guided by the static derivation path of the pre-selected action, which locates the action in the abstract syntactic tree of the current behaviour statically. This allows a considerable reduction of the search space. Such a technique often permits the analysis of divergent specifications that are generally beyond the capabilities of verification tools based on traces.