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 #x2018;Protocol validation algebra#x2019; by Holzmann, 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.
展开▼
