A toolbox for the verification of LOTOS programs
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Gregorio-Rodríguez, Joseph Sifakis · 1992
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.