|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: email@example.com , firstname.lastname@example.org|
|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.