Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Madelaine E., Ristori G. An exercise in protocol verification. In: 3rd Lotosphere Workshop & Seminar. (Pisa, Italy, 14 - 16 September 1992). Proceedings, vol. 2 T. Bolognesi, E. Brinksma, C.A. Vissers (eds.). CNUCE, 1992.
We present methods and tools for the verification of behaviours of Lotos programs, based on the explicit construction of a finite automaton. We discuss a behaviour oriented style for Lotos that eases the construction of this model. We present the verification tools integrated in the lite tool set, and illustrate the approach with the full specification and analysis of a datagram protocol.
Subject Network protocol
Program verification
Specifying and Verifying and Reasoning about Programs
Process calculus
Transition System
Behavioural semantics
Model Checking

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional