• DocumentCode
    2662256
  • 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
  • fYear
    1992
  • fDate
    0-0 1992
  • Firstpage
    246
  • Lastpage
    259
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Software Engineering, 1992. International Conference on
  • Conference_Location
    Melbourne, Australia
  • ISSN
    0270-5257
  • Print_ISBN
    0-89791-504-6
  • Type

    conf

  • DOI
    10.1109/ICSE.1992.753504
  • Filename
    753504
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2662256