Adequacy-preserving transformations of COSY path programs

Here we investigate a transformation of COSY path programs, which can be regarded as a refinment of a single event in one path program Q, using the specifications of the paths of another path program P. Such a transformation, called insertion, closely corresponds to refining an atomic action into several more elementary actions. In general, the path program resulting from the insertion of P into Q has behavioural properties quite different from those of P and Q. Therefore, in order to be able to use insertions as a verification tool, it is necessary to develop a set of rules which would guarantee the preservation of various dynamic properties through the insertion. One of such properties is adequacy, which captures the absence of partial deadlocks in a system. In this paper we present some sufficient conditions for adequacy-preserving insertion. Also, we fully characterise the set of all those programs P for which insertion is always adequacy-preserving.