A LOTOS Specification of a "Transit-Node"
Rapport SPECTRE, 94-8, VERIMAG, Grenoble, March 1994
This report describes the formal specification and
verification of a ``Transit-Node'', an abstraction of a
routing component of a communication network.
First, an informal definition of the Transit-Node,
initially proposed within the RACE project SPECS, is formally
described using the lotos language. Then, it is verified
following a model-based approach: the lotos specification is
translated into a finite LTS, and its correctness is checked
on this model.
Practically, all the verifications has been performed using CADP, a toolbox for the verification of lotos programs. This work was carried out in the framework of the French project ``VTT'' (Verification, Types and Time), those goal was to compare and evaluate different verification methods on a same case study.