Communication service specification using OOA and LOTOS

For the purpose of high reliability communication systems development, its service specification needs to be precisely described without any ambiguity. So, for specification, it is desirable to use LOTOS among the standard formal description techniques. LOTOS has been extensively used for formal description of protocols and telephone systems. In this paper we describe our approach and experience using OOA (Object-Oriented Analysis) as a means of easing the process of communication service specification development based on LOTOS. A communication service is first analyzed using an OOA technique. Then the results of the analysis are used to formally specify the service using LOTOS