Model-checking the Flooding Time Synchronization Protocol (2009)
Type of ContentConference Contributions - Published
PublisherUniversity of Canterbury. Electrical and Computer Engineering
AuthorsMcInnes, A.I.show all
Large-scale wireless sensor networks must be reliable, since they are intended to be operated without human intervention. Using well-understood building-blocks is one method of increasing confidence in the reliability of a sensor network design. In this paper, we use model-checking to analyze and characterize the Flooding Time Synchronization Protocol, a synchronization protocol that is distributed along with the TinyOS sensor network operating system. We apply a number of abstraction techniques to keep the model state-space small, and as a result are able to verify several properties of FTSP networks that have not previously been checked. Our results provide greater confidence in FTSP, and also establish some limitations on the size of FTSP networks. Our FTSP model provides a basis for further model-checking of FTSP.
CitationMcInnes, A.I. (2009) Model-checking the Flooding Time Synchronization Protocol. Christchurch, New Zealand: 7th IEEE International Conference on Control and Automation (IEEE-ICCA), 9-11 Dec 2009.
This citation is automatically generated and may be unreliable. Use as a guide only.