A Toolbox for the Verification of LOTOS Programs
Abstract
This paper presents the tools ALDEBARAN, CESAR, CESAR.ADT and CLEOPATRE which constitute a tool- box for compiling and verifying LOTOS programs. The principles of these tools are described, as well as their performances and limitations. Finally, the formal verification of the ret/REL atomic multicast protocol is given as an example to illustrate the practical use of the tool- box.
BibTeX
@inproceedings{Fernandez-al:ICSE92,
author = {Jean{-}Claude Fernandez and
Hubert Garavel and
Laurent Mounier and
Anne Rasse and
Carlos Rodr{\'{\i}}guez and
Joseph Sifakis},
title = {A Toolbox for the Verification of {LOTOS} Programs},
booktitle = {ICSE},
pages = {246--259},
publisher = {{ACM}},
year = {1992},
}