Title :
Transformation of Lotos specifications to Estelle specifications
Author :
El-Gendy, Haem ; Baraka, Hoda
Author_Institution :
GATIS Corp., Giza, Egypt
Abstract :
A technique for the 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 to 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 out areas for further research
Keywords :
ISO standards; computer aided software engineering; formal specification; minimisation; protocols; reachability analysis; specification languages; telecommunication computing; telecommunication standards; trees (mathematics); Estelle specifications; Lotos specifications; automated specification transformation; communications protocol; finite-state machine; infinite behaviour; minimization rule; reachability tree; restricted behaviour tree; specification size optimization; state number reduction; transition number reduction; Certification; Concurrent computing; Context; Costs; ISO standards; Natural languages; Protocols; Software systems; Testing;
Conference_Titel :
Computers and Communications, 1997. Proceedings., Second IEEE Symposium on
Conference_Location :
Alexandria
Print_ISBN :
0-8186-7852-6
DOI :
10.1109/ISCC.1997.615999
