A timed calculus for wireless systems

作者：Merro Massimo^*; Ballardin Francesco; Sibilio Eleonora

来源：Theoretical Computer Science, 2011, 412(47): 6585-6611.

DOI：10.1016/j.tcs.2011.07.016

• Wireless system
• Timed process calculus
• Local broadcast
• Communication collision

We propose a timed broadcasting process calculus for wireless systems where time-consuming communications are exposed to collisions. The operational semantics of our calculus is given in terms of a labelled transition system. The calculus enjoys a number of desirable time properties such as (i) time determinism: the passage of time is deterministic; (ii) patience: devices will wait indefinitely until they can communicate; (iii) maximal progress: data transmissions cannot be delayed, they must occur as soon as a possibility for communication arises. We use our calculus to model and study MAC-layer protocols with a special emphasis on collisions and security. The main behavioural equality of our calculus is a timed variant of barbed congruence, a standard branching-time and contextually-defined program equivalence. As an efficient proof method for timed barbed congruence we define a labelled bisimilarity. We then apply our bisimulation proof-technique to prove a number of algebraic laws.

• 出版日期2011-11-4