|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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. |
| Contact: | Luc Léonard Université de Liège Institut d'Electricité Montefiore, B28 B-4000 Liège 1 BELGIUM Tel (direct line): +32 (41) 664992 Tel (secretary): +32 (41) 662691 Fax: +32 (41) 662989 E-mail: leonard@montefiore.ulg.ac.be |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page