An issue of current interest in the Open System Interconnection (OSI) field is the choice of a language well suited to specification and verification. For this purpose, two languages based on R. Milner's communication calculi are proposed, respectively intended for the specification of asynchronous and synchronous OSI systems. A formal verification method, relying upon the algebraic foundations of the two languages, is introduced and illustrated by means of examples based on nontrivial protocols and services.
ECCS and LIPS: Two Languages for OSI Systems Specification and Verification
CARCHIOLO, Vincenza;DI STEFANO, Antonella;PAPPALARDO, Giuseppe
1989-01-01
Abstract
An issue of current interest in the Open System Interconnection (OSI) field is the choice of a language well suited to specification and verification. For this purpose, two languages based on R. Milner's communication calculi are proposed, respectively intended for the specification of asynchronous and synchronous OSI systems. A formal verification method, relying upon the algebraic foundations of the two languages, is introduced and illustrated by means of examples based on nontrivial protocols and services.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
