Correct-by-Construction and Optimal Synthesis of Beacon-Enabled ZigBee Network

In this paper we develop a formal approach for the synthesis of a cost-effective and correct-by-construction communication network (focusing on ZigBee wireless networks) subject to a set of end-to-end communication constraints of latency, bandwidth and error-rate, together with the constraints of the network protocols and the desired geographical placement of the network. We also develop a software platform to implement the proposed approach for network synthesis, and apply it to a practical wireless network synthesis for centralized as well as distributed estimation application.