ECCS and LIPS: two languages for OSI systems specification and verification

1 April 1989

journal article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems

Vol. 11 (2) , 284-329
https://doi.org/10.1145/63264.63402

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.

Keywords

This publication has 10 references indexed in Scilit:

Extensional equivalences for transition systems
Acta Informatica, 1987
A LOTOS Specification of the PROWAY Highway Service
IEEE Transactions on Computers, 1986
A Theory of Communicating Sequential Processes
Journal of the ACM, 1984
Specifying Concurrent Program Modules
ACM Transactions on Programming Languages and Systems, 1983
Calculi for synchrony and asynchrony
Theoretical Computer Science, 1983
Proving Liveness Properties of Concurrent Programs
ACM Transactions on Programming Languages and Systems, 1982
A proof technique for communicating sequential processes
Acta Informatica, 1981
A Calculus of Communicating Systems
Lecture Notes in Computer Science, 1980
Formal verification of parallel programs
Communications of the ACM, 1976
An axiomatic proof technique for parallel programs I
Acta Informatica, 1976