PUMA
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.
 
 
Abstract
(English)
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
Parallelism
Concurrency
LOTOS
Transition System
Behavioural semantics
Automata
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