Loading...
Please wait, while we are loading the content...
Similar Documents
Using integer clocks to verify the timing-sync sensor network protocol.
| Content Provider | CiteSeerX |
|---|---|
| Author | Huang, Xiaowan Singh, Anu Smolka, Scott A. |
| Abstract | We use the UPPAAL model checker for Timed Automata to verify the Timing-Sync time-synchronization protocol for sensor networks (TPSN). The TPSN protocol seeks to provide network-wide synchronization of the distributed clocks in a sensor network. Clock-synchronization algorithms for sensor networks such as TPSN must be able to perform arithmetic on clock values to calculate clock drift and network propagation delays. They must be able to read the value of a local clock and assign it to another local clock. Such operations are not directly supported by the theory of Timed Automata. To overcome this formal-modeling obstacle, we augment the UPPAAL specification language with the integer clock derived type. Integer clocks, which are essentially integer variables that are periodically incremented by a global pulse generator, greatly facilitate the encoding of the operations required to synchronize clocks as in the TPSN protocol. With this integer-clock-based model of TPSN in hand, we use UPPAAL to verify that the protocol achieves network-wide time synchronization and is devoid of deadlock. We also use the UPPAAL Tracer tool to illustrate how integer clocks can be used to capture clock drift and resynchronization during protocol execution. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Integer Clock Sensor Network Timing-sync Sensor Network Protocol Tpsn Protocol Local Clock Timed Automaton Clock Drift Integer-clock-based Model Formal-modeling Obstacle Protocol Execution Timing-sync Time-synchronization Protocol Distributed Clock Uppaal Specification Language Uppaal Model Checker Clock Value Network-wide Time Synchronization Network-wide Synchronization Global Pulse Generator Integer Variable Network Propagation Delay Uppaal Tracer Tool Clock-synchronization Algorithm |
| Content Type | Text |
