|
| 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 |
A LOTOS Specification of a "Transit-Node"
Laurent Mounier
Rapport SPECTRE, 94-8, VERIMAG, Grenoble, March 1994
Abstract:
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 |  |
 PostScript |