کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
434309 | 1441700 | 2013 | 20 صفحه PDF | دانلود رایگان |
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.
► A formal modeling language for mobile systems with stateful channels is proposed.
► Reduction and labeled transition semantics for PiZ is provided.
► A motivating example of modeling the hidden node problem in PiZ is provided.
► It is proved that the labeled tau-transitions match reductions for PiZ.
► It is proved that bisimilarity for PiZ is closed under important operators.
Journal: Science of Computer Programming - Volume 78, Issue 9, 1 September 2013, Pages 1470–1489