Database of Case Studies Achieved Using CADP

"Transit Node" Message Router

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 : [email protected]
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

Last modified: Thu Feb 11 12:42:30 2021.

Back to the CADP case studies page