Une Boîte à Outils pour la Verification de Programmes LOTOS.

Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, Joseph Sifakis

Actes du Colloque Francophone pour l'Ingénierie des Protocoles CFIP'91 (Pau, France), 479-500, September 1991

Abstract:

Cet article présente les logiciels ALDEBARAN, CAESAR, CAESAR.ADT et CLEOPATRE qui constituent une boîte à outils pour la compilation et la vérification de programmes LOTOS. Les principes de fonctionnement des différents outils sont exposés, ainsi que leurs performances et leurs limitations respectives.
L'utilisation pratique de la boîte à outils est illustrée par un exemple de vérification formelle du protocole de diffusion atomique rel/REL.

22 pages, in French.

PDF

PostScript