Title :
A Toolbox For The Verification Of LOTOS Programs
Author :
Fernandez, Jean-Claude ; Garavel, Hubert ; Mounier, Laurent ; Rasse, A. ; Rodriguez, Carlos ; Sifakis, Joseph
Author_Institution :
LGI-IMAG
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.
Keywords :
Automata; Control system synthesis; Distributed control; Electronic mail; Hardware design languages; Logic; Multicast protocols; Partial response channels; Real time systems;
Conference_Titel :
Software Engineering, 1992. International Conference on
Conference_Location :
Melbourne, Australia
Print_ISBN :
0-89791-504-6
DOI :
10.1109/ICSE.1992.753504
