Utilisation de CAESAR et ALDEBARAN

Hubert Garavel

Compilation et vérification de programmes LOTOS, Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989

part of thesis (appendices C and D of [Garavel-89-b]) Two examples of using LOTOS to specify and CAESAR/ALDEBARAN to verify: an extended alternating bit protocol and a family of systolic arrays computing the convolution product

24 pages, in French

PDF

PostScript