An operational semantics for a calculus for wireless systems

作者：Lanese Ivan^*; Sangiorgi Davide

来源：Theoretical Computer Science, 2010, 411(19): 1928-1948.

DOI：10.1016/j.tcs.2010.01.023

• Wireless systems
• Broadcast
• Reduction Semantics
• Labelled Transition Semantics
• Interference

In wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. We develop an operational semantics for a calculus of wireless systems. We present different Reduction Semantics and a Labelled Transition Semantics and prove correspondence results between them. Finally, we apply CWS to the modelling of the Alternating Bit Protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework.
A major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. Such interference occurs when a location is simultaneously reached by two transmissions. The Reduction Semantics differ on how information about the active transmissions is managed.
We use the calculus to describe and analyse a few properties of a version of the Alternating Bit Protocol.

• 出版日期2010-4-6
• 单位INRIA