Abstract:

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.