Contribution to the specification in Z of concurrency under a non-interleaving semantics

The traditional approach for specifying concurrent systems using Z is based on an interleaving model of concurrency. We show how to specify in Z a concurrent model with shared variables based on a non interleaving semantics. At the static level each concurrent program is formalized by an abstract data type. The behaviour of the system is described by a causal or a parallel transition system which is specified in Z in terms of the allowable sequence of state changes that result from the execution of one or more actions in parallel. Some solutions are also proposed to specify parallel actions as well as the choice between conflicting actions