Verification and Performance Evaluation of S-MAC Protocol Based on Process Calculi

Author

Abo, Robert ; Barkaoui, Kamel ; Djouani, Karim

Author_Institution

Lab. Cedric, Conservatoire Nat. des Arts et Metiers, Paris, France

fYear

2010

fDate

21-25 June 2010

Firstpage

189

Lastpage

198

Abstract

This paper relates to the formal analysis of S-MAC, a medium-access protocol designed for wireless sensor networks. We study the synchronization mechanism of mobile nodes and the 4-way handshake mechanism of the Carrier Sense Multiple Access with Collision Avoidance scheme implemented by S-MAC. We model these previous mechanisms with the π-calculus and the proof of their deadlocks-freeness is achieved by using the Mobility Workbench tool. A performance evaluation of S-MAC is also conducted by modeling and simulating the communications between fixed nodes with the Performance Evaluation Process Algebra (PEPA). The performance measurements are carried-out with the PEPA Eclipse plug-in.

Keywords

access protocols; carrier sense multiple access; performance evaluation; process algebra; synchronisation; wireless sensor networks; PEPA Eclipse plug-in; S-MAC protocol; carrier sense multiple access; collision avoidance; four way handshake mechanism; medium access protocol; mobile nodes; performance evaluation process algebra; process calculi; synchronization mechanism; wireless sensor network; Communication channels; Mobile communication; Protocols; Receivers; Schedules; Synchronization; Wireless sensor networks; PEPA; Pi-calculus; S-MAC; performance evaluation; process calculi;

fLanguage

English

Publisher

ieee

Conference_Titel

Distributed Computing Systems Workshops (ICDCSW), 2010 IEEE 30th International Conference on

Conference_Location

Genova

ISSN

1545-0678

Print_ISBN

978-1-4244-7471-4

Type

conf

DOI

10.1109/ICDCSW.2010.54

Filename

5628762