<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>8327</REFNUM><AUTHORS><AUTHOR>Ballarini,P.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2006</YEAR><TITLE>(Towards) Model Checking Medium Access Control for Sensor Networks</TITLE><PLACE_PUBLISHED>Proceedings of the second international symposium on leveraging applications of formal methods</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><PAGES>256-262</PAGES><LABEL>Ballarini:2006:8327</LABEL><KEYWORDS><KEYWORD>Verification</KEYWORD></KEYWORDS<ABSTRACT>We describe initial attempts to verify S-MAC, a medium access control protocol designed for wireless sensor networks, by means of the PRISM model checker. The S-MAC protocol is built on top of the IEEE 802.11 standard for wireless ad hoc networks and, as such, it uses the same randomised backoff procedure as a means to avoid collision. In order to minimise energy consumption, in S-MAC, nodes are periodically put into a sleep state, Synchronisation of the sleeping schedules is necessary for the nodes to be able to communicate. Intuitively, energy saving obtained through a periodic sleep mechanism will be at the expense of performance. In previous work on S-MAC verification, a combination of analytical techniques and simulation has been used to confirm the correctness of this intuition for a simplified (abstract) version of the protocol in which the initial schedules coordination phase is assumed correct. We discuss initial steps towards applying model checking to the S-MAC protocol. Our aim is twofold: to confirm the results that refer to the abstract version of the protocol and to study the effect of coordinated sleeping on the protocol performance.</ABSTRACT></RECORD></RECORDS></XML>