[Excerpt from INRIA 1996 Annual Report]

CADP/EUCALYPTUS: A TOOLBOX FOR PROTOCOL ENGINEERING

The SPECTRE/VASY project developed a toolbox for the design and debugging of protocals and distributed systems. This toolbox is based on the LOTOS language (ISO 8807 standard). It offers simulation, code generation, partial or exhaustive verification capabilities that make it possible to detect potential design errors in complex systems at the earliest stage, thus resulting in improved reliability and lower development costs.

This toolbox was distributed to more than 125 sites worldwide and was used in several practical situations. Among the most recent that are worth mentioning are the analysis of the BRP protocol used by Philips for one of their audiovisual products (INRIA), the study of election distributed algorithms on a ring network (INRIA), the analysis of railroad configurations (SICS, Sweden), the characterization of an error in the TCP protocol (GMD-FOKUS, Germany), the study of interactions between telephone services (CWI, Netherlands) as well as the breaking of the Equicrypt security protocol, based on the "trustworthy third party" principle and designed to control access to multimedia services (University of Liège, Belgium).

The toolbox is also used for the verification of multiprocessor architectures developed by Bull in the framework of the VASY initiative of the Bull/INRIA DYADE GIE. In particular, it was used to prove the correctness of the bus arbiter of the PowerScale architecture for the Bull Escala workstations and servers. Current work concerns the cache coherence protocol of the future multiprocessor architecture that will equip top of the line Bull machines.

Back to the VASY Home Page