next up previous

Final Report of the COST-247 Action

About compositional verification of TLA protocol specifications using projections

Tatjana Kapus, Zmago Brezocnik

Faculty of Electrical Engineering and Computer Science
University of Maribor
Smetanova ul. 17, SI-2000 Maribor, Slovenia
Email: ,
Tel: +386 62 221-112
Fax: +386 62 225-013


A common approach to reduce the complexity of the verification of a concurrent system or algorithm is to decompose it into smaller parts and to verify each part separately. Although communication protocol entities typically perform several distinct functions, it has long been observed that it is often difficult to decompose them into smaller separate modules for handling each function because they share variables and/or messages. The method of projections has been proposed as an alternative. We show how projections can be performed in combination with compositional proof rules for verifying (interleaving) parallel compositions of components specified in the style of TLA. In fact, projection is implication.

This presentation has been given during the COST-247 9th Management Committee Meeting (Antalya, Turkey, November 4--5, 1996).

COST-247 Working Group(s):

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page