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: https://doi.org/10.1016/j.scico.2012.10.010
Url : http://www.sciencedirect.com/science/article/pii/S0167642312001955
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: https://doi.org/10.1016/j.scico.2012.10.010