|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
VERIMAG and INRIA Rhone-Alpes (FRANCE)
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Networks and Communication Protocols.
|
| Period: |
1994
|
| Size: |
350 lines
|
| Description: |
This case-study deals with a message router ("Transit Node") chosen
by the European RACE project SPECS as a common example for comparing
various formal description techniques. Starting from an informal definition of a "Transit Node" (an abstraction of a routing component of a communication network), a formal description in LOTOS was produced. This description was verified using a model-based approach : the LOTOS description is translated into a finite Labelled Transition System (LTS), which was abstracted in different ways (by considering as visible only a subset of its transitions) and compared to various simpler labelled Transition Systems expressing the properties to be verified. The comparison was done using the bisimulation equivalences and preorders. To avoid state explosion, a "compositional approach" was used: the Transit Node description was divided into 5 sub-processes; for each of them, the corresponding Labelled Transition System was generated seperately, then minimized before being composed with the others. |
| Conclusions: |
LOTOS proved to be adequate for describing the Transit Node formally.
Choosing a "process algebraic" formalism like LOTOS naturally leads to
an operational description of the system. Using the CADP tools, all of the properties specified for the Transit Node have been validated (or, in some cases, proven to be false). |
| Publications: |
Laurent Mounier, "A LOTOS specification of a Transit-Node",
Rapport SPECTRE 94-8, VERIMAG, Grenoble, March 1994.
Available on-line from
http://cadp.inria.fr/publications/Mounier-94.html
and from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Laurent Mounier VERIMAG Centre Equation 2, avenue de Vignate F-38610 Gieres FRANCE tel : +(33) 4 76 63 48 52 fax : +(33) 4 76 63 48 50 E-mail : Laurent.Mounier@imag.fr |
| Further remarks: |
The source code of this case-study as well as explanations on the
verification with CADP is available on-line at:
http://cadp.inria.fr/ftp/demos/demo_18
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