Modeling mobile stateful channels in Z

We investigate a principled extension of the -calculus for formal modeling of mobile communicating systems with stateful channels. In our proposed extension, called Z, a channel is associated with a stateful abstract type in the Z specification language. We develop both reduction as well as labeled transition semantics for Z. We show that the important properties of the -calculus are preserved in Z: (1) -transitions match reductions; and (2) bisimilarity induced by the labeled transitions is closed under parallel composition, name restriction, and a restricted recursion. The paper illustrates the use of stateful channels by modeling the ‘hidden node problem’ in a wireless network.