Analysis of a clock synchronization protocol for wireless sensor networks

DOI10.1016/J.TCS.2011.07.018zbMath1307.68009OpenAlexW2109069777MaRDI QIDQ764293

Julien Schmaltz, Faranak Heidarian, Frits W. Vaandrager

Publication date: 13 March 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.07.018

zbMATH Keywords

theorem provingtimed automatamodel checkingindustrial application of formal methodswireless sensor networksclock synchronization algorithms

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Distributed systems (68M14) Network protocols (68M12)

Related Items (4)

Shrinking timed automata ⋮ Target-synchronization of the distributed wireless sensor networks under the same sleeping-awaking method ⋮ Multi-scale verification of distributed synchronisation ⋮ A Filter‐based Clock Synchronization Protocol for Wireless Sensor Networks

Uses Software

• PRISM
• Isabelle/HOL
• Uppaal
• Automath
• Mcmt

Cites Work

• Analysis of a biphase mark protocol with Uppaal and PVS
• Methods, models and tools for fault tolerance
• Isabelle/HOL. A proof assistant for higher-order logic
• Gradient clock synchronization
• Integrated formal methods. 6th international conference, IFM 2007, Oxford, UK, July 2--5, 2007. Proceedings.
• Time, clocks, and the ordering of events in a distributed system
• A formally verified algorithm for clock synchronization under a hybrid fault model
• Formal Methods for the Design of Real-Time Systems
• MCMT: A Model Checker Modulo Theories

This page was built for publication: Analysis of a clock synchronization protocol for wireless sensor networks