… Accordingly, we obtain the condition for deadlock free system as Q=¬∀i•( in (n i . rts )∨ in
(n i . rec )) that must remain invariant during the lifetime of the system. To achieve deadlock
freedom, we look into the transition rule(s) which includes the prohibitive system states in their
post-conditions. The first transition rule n i .r 1 in the node process changes its state from n i .rtr
to n i .rec. It may be shown that the rule would have the following two guards corresponding
to the two sub-rules n i .r 1 1 and n i .r 1 2 . … Hence, we propose to disconnect the user …

Method for the derivation of a correct deadlock free communication kernel for loop
connected message passing architecture from its user's specification is described. Dijkstra's
weakest pre-condition approach is used as the specification language. This specification is
augmented by including the property constrains which are necessary for the system. Iterative
augmentation derives an almost completed design. The construction achieved by this
method is ensured to be correct. The method is illustrated by an example. Introduction: Many …