Database of Case Studies Achieved Using CADP

OSI95 Enhanced Transport Service Specification (ETSS).

Organisation: University of Liège (BELGIUM), within the OSI95 project.

Method: LOTOS

Tools used: The specification has been verified with regard to its syntax and its static semantics by the use of the LITE tool, a product from the ESPRIT-II Lotosphere consortium. Nevertheless, it has neither been tested nor completely simulated yet, which would require, with the existing tools and for a specification of such a size, a lot of time. Just some sub-processes have been partially simulated by means of the SMILE simulator of LITE. On the other hand, after extensive transformation work, a subset of this specification has passed successfully through the CADP toolset from INRIA Rhône-Alpes (Grenoble).

Domain: Networking Management.

Period: 1992

Size: about 4500 lines of LOTOS (50% for data types)
1 man/year

Description: The work addressed the LOTOS specification of a new Transport Service, which was designed to meet the new needs raised by the development of multimedia applications and of high-speed networks. The specification was written by a single worker, in the constraint-oriented style. Unlike what usually happens, this specification was not the translation in LOTOS of an already existing and well defined system. It was developed in parallel with the design phase of the specified Transport Service. Its evolution followed the design of the Service. The LITE tool was used for the syntactic and semantic checking. Several attempts were made to simulate the specification with the SMILE tool, but this happened to be extremely time and resource consuming. Just obtaining the possible two first steps for a the behaviour of a connection establishment required around 5 hours and 280 MB of swap-space on a stand-alone SPARC1+.

Conclusions: Developing the specification in parallel with the, sometimes chaotic, design phase of the specified system made the life of the specifier harder. He often faced unclarities, or even inconsistencies and had to fix details the designers had never thought about. On the other hand, all this feedback was of great benefit to the designers. It helped them in getting faster a clearer view of their own ideas and pointed out many potential problems. The global result was considered positive. The publication below presents a more complete discussion about the writing of this spec. The specification is given in annex.

Publications: [Leonard-94] Luc Léonard. "The LOTOS specification of the Enhanced Transport Service". In André Danthine, editor, OSI95 Transport Service with Multimedia Support, pages 239-244, 398-515, Springer-Verlag, 1994.
Luc Léonard
Université de Liège
Institut d'Electricité Montefiore, B28
B-4000 Liège 1
Tel (direct line): +32 (41) 664992
Tel (secretary): +32 (41) 662691
Fax: +32 (41) 662989

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Jul 17 15:55:41 2014.

Back to the CADP case studies page