VERIMAG and INRIA Rhone-Alpes (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
Networks and Communication Protocols.
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.
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).
Laurent Mounier, "A LOTOS specification of a Transit-Node",
Rapport SPECTRE 94-8, VERIMAG, Grenoble, March 1994.
Available on-line from
and from our FTP site in PDF or PostScript
2, avenue de Vignate
tel : +(33) 4 76 63 48 52
fax : +(33) 4 76 63 48 50
E-mail : Laurent.Mounier@imag.fr
The source code of this case-study as well as explanations on the
verification with CADP is available on-line at:
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies