Transformation of Lotos specifications to Estelle specifications

In this paper, a technique for automated transformation of a Lotos specification to an Estelle specification is presented. First, a Restricted Behaviour Tree is constructed from the Lotos specification in a somewhat similar way as generating a reachability tree for a finite state machine. The Restricted Behaviour Tree has a finite size even when the communications protocol specified represents infinite behaviour. We develop an algorithm for constructing the Estelle specifications from the Restricted Behaviour Tree. A minimization rule is also developed to optimize the size of the Estelle specification by reducing both the number of states and the number of transitions. We conclude by pointing areas for further research.