ECCS and LIPS: Two Languages for OSI Systems Specification and Verification

Abstract

An issue of current interest in the Open Systems Interconnection (OSI) field is the choice of a language well suited to specification and verification. For this purpose, two languages based on 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.