Regular PapersNo Access

FORMAL METHOD FOR AUTOMATED TRANSFORMATION OF LOTOS SPECIFICATIONS TO ESTELLE SPECIFICATIONS

HAZEM EL-GENDY

Ministry of Awkaf, Cairo, Egypt

Search for more papers by this author

and

NABIL EL-KADHI

EpiTech, 14/16 Rue Voltaire 94270 Kremelin Bicetre, France

Search for more papers by this author

https://doi.org/10.1142/S0218194005002567Cited by:3 (Source: Crossref)

Abstract

ISO and IEC have jointly developed two Formal Description Techniques (FDTs) for specifying distributed real time systems such as computer/telecommunications protocols. These are Lotos and Estelle. In this paper, a formal method for automated transformation of a Lotos specification to an Estelle specification is presented. The method is applicable to various Lotos specification styles and to various communications protocols of ISO OSI layers.

Our method has applications in conformance testing of such systems and building common semantic model for the various FDTs. In this paper, we develop an algorithm for constructing a 'Data Oriented'-Restricted Behavior Tree T that represent both the control flow aspects and the data flow aspects of the system. Then, we develop an algorithm for constructing the Estelle specifications from T. 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.

Keywords:

References

ISO/IEC 8807, Information Processing Systems — Open Systems Interconnection: LOTOS — A Formal Description Technique Based on Temporal Ordering of Observational Behaviour, 1992 . Google Scholar
H. El-Gendy, H. El-Sayed, and A. Fayez, Equivalence of behaviour specifications of processes, in Proc. Int. Conf. on Telecommunications, Chalkidiki, Greece, 22–25 June 1998, pp. 171–175 . Google Scholar
H. El-Gendy, H. El-Sayed, and A.-W. Fayez, Comparative analysis of the notions of equivalence of process specifications, in Proc. Int. Symp. for Computers and Communications, Athens, Greece, June 30–July 2, 1998, pp. 711–716 . Google Scholar
H. El-Gendy, A new theory for equivalence between process specifications, in Proc. IEEE Int. Conf. on Electronics, Circuits, and Systems, Rodous, Greece, October 16–18, 1996, pp. 1186-1189. Was also accepted for publication in the Proc. Int. Conf. on Networks, Orlando, Florida, USA, Jan. 8–10, 1996 . Google Scholar
H. El-Gendy, A new method for deriving test sequences for protocols specified in Lotos, in Proc. Int. Conf. on Networks, Orlando, Florida, USA, January 8–10, 1996, pp. 205–208 . Google Scholar
H. El-Gendy and O. Abou-Rabia, Derivation of test sequences for protocols specified in Lotos, in Proc. IEEE Int. Conf. on Electronics, Circuits, and Systems, Amman, Jordan, December 1995, pp. 220–225 . Google Scholar
H. Saiedian, An Invitation to Formal Methods (IEEE Computer, 1996) pp. 16–30. Google Scholar
H. El-Gendy and H. Baraka, Transformation of Lotos specifications to Estelle-based specifications, in Proc. Int. Symp. on Computers and Communications, Alexandria, Egypt, July 1–3, 1997, pp. 215–220 . Google Scholar
T. Bolognesi, F. Lucidi and S. Trigila, Journal of Computer Standards and Interfaces 16, 87 (1994). Web of Science, Google Scholar
C. M. Araset al., Proc. IEEE 82(1), 122 (1994). Web of Science, Google Scholar
M. Sigireanu and R. Mateescu, Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (FierWire): An Experiment with E-Lotos, INRIA Technical Report No. 3172, 1997. A short version of this report is also available in Ignac Lovrek (ed.), Proc. COST 247 2nd International Workshop on Applied Formal Methods in System Design, Zagreb, Croatia, June 1997 . Google Scholar
A. Dahbura and K. Sabnani, Proc. IEEE 78(8), 1317 (1990). Web of Science, Google Scholar
D. Sidhu and T. Leung, IEEE Trans. on Software Engineering 15(4), 413 (1989). Web of Science, Google Scholar
M. S. Bloor and J. Owen, Journal of Computer Standards and Interfaces 17, 231 (1995). Web of Science, Google Scholar
C.-Y. Chang and S.-C. Tu, Journal of Network and Computer Applications 25(3), 161 (2002). Web of Science, Google Scholar
S. Farahvash, K. Akhavan and M. Kavehrad, Int. J. Wireless Information Networks 9(3), 165 (2002). Web of Science, Google Scholar
J. Q. Bao and L. Tong, IEEE Journal on Selected Areas in Communications 18(3), 418 (2000). Web of Science, Google Scholar
D. P. A. Greenwood and R. A. Carrasco, IEE Proceedings Communications 147(5), 285 (2000). Web of Science, Google Scholar
H. El-Gendy, Using formal methods: Importance and experience, in Proc. 2nd Int. Conf. on Computer Science, Software, Information Technology, e-Business, and Applications, June 5–7, 2003 . Google Scholar
G. Bochmann, Specifications of a simplified transport protocol using different formal description techniques, Technical Report #623, Department D'Informatique, University De Montreal, April 1987. Also in the Journal of Computer Networks and ISDN Systems 18(5) (1990) 335–377 . Google Scholar
J.-P. Wu and S. T. Chanson, Translation from Lotos and Estelle specifications to extended transition system and its verification, in Proc. IFIP Forte 89, Vancouver, B.C., Canada, Dec. 1989 . Google Scholar
ISO/IEC 9074, Information Processing Systems — Open Systems Interconnection: ESTELLE — Formal Description Technique Based on an Extended State Transition Model, 1992 . Google Scholar
H. El-Gendy, H. El-Sayed, and A.-W. Fayez, Transformation of Estelle specification into Lotos specifications, in Proc. 13th Int. Conf. on Computers and Their Applications, Honolulu, Hawaii, USA, March 25–27, 1998, pp. 82–84 . Google Scholar
H. El-Gendy, Towards a foundation for FDT-based conformance testing requirements, in Proc. IEEE Int. Conf. on Electronics, Circuits, and Systems, Rodous, Greece, October 16-18, 1996, pp. 1182–1185. Was also accepted for publication in the Proc. Int. Conf. on Networks, Orlando, Florida, USA, January 8–10, 1996 . Google Scholar
H. El-Gendy, Testing data flow aspects of communications protocols, software, and systems specified in Lotos, in Proc. Int. Conf. on Computer Science, Software, Information Technology, e-Business, and Applications, Rio de Janeiro, Brazil, June 5–7, 2003 . Google Scholar
H. El-Gendy and N. El Kadhi, Using formal methods: Importance, experience, and comparative analysis, accepted for publications in the Int. Journal on Computing Methods in Science and Engineering, published in Greece, 2005 . Google Scholar
H. El-Gendy and N. El Kadhi, Characteristics of conformance testing equivalence, in Proc. 3rd Int. Conf. on Computer Science, Software Engineering, Information Technology, e-Business, and Applications, Cairo, Egypt, Dec. 27–29, 2004. It has also been recommended for journal publication . Google Scholar