A Toolbox for the Verification of LOTOS Programs.

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

Proceedings of the 14th International Conference on Software Engineering ICSE'14 (Melbourne, Australia), pages 246-259, May 1992


This paper presents the tools ALDEBARAN, CAESAR, CAESAR.ADT and CLEOPATRE which constitute a toolbox 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 rel/REL atomic multicast protocol is given as an example to illustrate the practical use of the toolbox.

14 pages