A LOTOS Specification of a "Transit-Node"

Laurent Mounier

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.

39 pages