Journal
THEORETICAL COMPUTER SCIENCE
Volume 413, Issue 1, Pages 87-105Publisher
ELSEVIER
DOI: 10.1016/j.tcs.2011.07.018
Keywords
Industrial application of formal methods; Clock synchronization algorithms; Timed automata; Model checking; Theorem proving; Wireless sensor networks
Categories
Funding
- European Community [214755 (QUASIMODO)]
Ask authors/readers for more resources
The Dutch company Chess develops a wireless sensor network (WSN) platform using an epidemic communication model. One of the greatest challenges in the design is to find suitable mechanisms for clock synchronization. In this paper, we study a proposed clock synchronization protocol for the Chess platform. First, we model the protocol as a network of timed automata and verify various instances using the Uppaal model checker. Next, we present a full parametric analysis of the protocol for the special case of cliques (networks with full connectivity), that is, we give constraints on the parameters that are both necessary and sufficient for correctness. These results have been checked using the proof assistant Isabelle. We report on the exhaustive analysis of the protocol for networks with four nodes, and we present a negative result for the special case of line topologies: for any instantiation of the parameters, the protocol will eventually fail if the network grows. (C) 2011 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available