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.