Symbolic execution of LOTOS specifications.

Abstract

LOTOS (Language Of Temporal Ordering Specification) is a Formal description Technique (FDT) based on the temporal ordering of observational behaviour. It was developed by ISO (International Organization for Standardization) for the specification of OSI (Open System Interconnection) services and protocols. This thesis presents a method of translating a LOTOS specification written in any given style into either of two simpler forms, known as the Monolithic Style Specification and the Parameterized Tree. A method of applying LOTOS expansion theorems to derive an intermediary form, known as the Behaviour Tree, is described first. A Reduction Algorithm, based on a subset of congruence rules, has been developed to provide a means to eliminate superfluous internal events and branches in the Behaviour Tree prior to conversion to either of the two simpler forms. Methods of transforming the reduced Behaviour Tree to either the Monolithic Style Specification ar Parameterized Tree have been developed. A tool has been developed to demonstrate these concepts. To show the application of this tool, we discuss a method for obtaining test cases from a Monolithic Style Specification. Finally, a method to translate such test cases into TTCN form has been outlined.