|
| 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 |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Universidade Federal de Santa Catarina (UFSC), Brasil
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes) TOPO |
| Domain: |
Network Management.
|
| Period: |
1996-1997
|
| Size: |
|
| Description: |
The goal of proactive network management is to prevent problems that can
happen in networks and avoid them from having an impact on the service
offered to users, by detecting them before they occur. Formal description techniques, and LOTOS in particular, can be used in proactive network management for specifying the behaviour of "proactive agents", i.e. processes that control and analyze network traffic. In order to ease the elaboration of new proactive agents, a library of re-usable components has been developed at UFSC. This library (named "bibLOTOS") contains LOTOS types and processes that can be used as building blocks for specifying proactive agents, together with informal descriptions, C code and transition systems generated by the CADP tools. The library itself is implemented as a Microsoft Access database. The bibLOTOS library has been used to specify a proactive agent responsible for controlling traffic in a network. The specification was then exhaustively simulated using the CADP tools, then interactively simulated, executed, checked for deadlocks, and compared to the service graph modulo observation equivalence. |
| Conclusions: |
The specification task is greatly helped by the use of bibLOTOS
predefined constructs. The CADP tools are useful for checking the
correctness of the specification built with the predefined constructs.
|
| Publications: |
Mirela Sechi Moretti Annoni Notare, Bernardo Goncalvez Riso,
Paulo Sergio Lorena, Manoel Camillo de Olivera Penna Neto,
Carlos Becker Westphall
Formal Design of a Telecommunication Network Management System
IEEE ISCC97 (Egypt, Alexandria, 1-3 July 1997)
Cristiano Maciel, Elenirse M. Furlanetto, Mirela Notare, Bernardo Riso, Carlos Westphall "bibLOTOS: Une bibliotheque de constructions predefinies pour un projet de gestion de reseau", Technical Report, Universidade Federal de Santa Catarina (UFSC), Brasil. |
| Contact: | Mirela Sechi Moretti Annoni Notare Universidade Federale de Santa Catarina (UFSC) Technological Center / Department of Computer Sience (CTC/INE) Network and Management Laboratory (LRG) P.O. Box 476 - ZIP 88040-970 Florianopolis SC, Brazil Tel: +55 (48) 231-9498 Fax: +55 (48) 231-9770 E-mail: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page