Automatic Generation of Wireless Sensor Networks Scheduling

In this paper, the Discrete Controller Synthesis (DCS) technique is applied in order to obtain a correct-by- construction automatic distributed scheduling of Wireless Sensor Network (WSN). Our approach starts from an abstract formal model considering that communication between nodes are instantaneous. Then, a refined model is obtained by adding a realistic communication mechanism while preserving the global controlled behavior generated initially by automatic synthesis. This communication mechanism is called a synchronization “barrier“: a software mechanism constraining a set of sensors to wait for each other before making its own local decision and before deactivation. The approach is illustrated by a WSN model with two communicating nodes.