An extended algebra for the validation of communication protocols

Author

Lombard, A. ; Palazzo, S.

Author_Institution

Fac. di Ingegneria, Catania Univ., Italy

Volume

4

Issue

3

fYear

1989

fDate

5/1/1989 12:00:00 AM

Firstpage

148

Lastpage

158

Abstract

This paper presents a simple algebra for the validation of communication protocols modelled as state-transition systems. It is based on an original extension to the Protocol validation algebra by Holzmann (1982), enhanced with additional facilities such as operators for handling parallelism among communicating processes and rules for obtaining the specification of a composed process from those of the components. The semantics of the algebraic operators provide for a validation technique, through which some protocol properties can be verified, such as termination, deadlock freeness, livelock freeness, absence of residuals and conformity of the protocol to the service. A brief description of a software tool which implements the method is given

Keywords

computer communications software; finite automata; formal specification; program verification; protocols; software tools; Protocol validation algebra; algebraic operators; communicating processes; communication protocols; deadlock freeness; extended algebra; finite automata; formal description; livelock freeness; parallelism; protocol properties; semantics; software tool; state-transition systems; termination;

fLanguage

English

Journal_Title

Software Engineering Journal

Publisher

iet

ISSN

0268-6961

Type

jour

Filename

42930