Back close

Modeling mobile stateful channels in PiZ

Publication Type : Journal Article

Thematic Areas : Amrita Center for Cybersecurity Systems and Networks

Publisher : Elsevier

Source : Science of Computer Programming 78(9): 1470-1489, 2013, Elsevier. DOI:

Url :

Keywords : Abstract type, Bisimilarity, Mobility, Process algebra, Stateful channel, Z language

Campus : Amritapuri, Coimbatore

School : Centre for Cybersecurity Systems and Networks, School of Engineering

Center : Cyber Security

Department : cyber Security

Year : 2013

Abstract : 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.

Cite this Research Publication : J. Poroor and B. Jayaraman, “Modeling mobile stateful channels in PiZ”, Science of Computer Programming, Science of Computer Programming 78(9): 1470-1489, 2013, Elsevier. DOI:

Admissions Apply Now