Schedule Synthesis for Time-Triggered Multi-hop Wireless Networks with Retransmissions

In wireless networks, a message is dropped unexpectedly due to the physical phenomena such as fading, thus requiring a number of backup retransmissions. However, retransmission (which is known to be probabilistic) is mostly disabled in the design of time-triggered communication by the precomputed schedule that reserves every transmission tightly. In this paper, we formally specify the scheduling constraints for a time-triggered wireless network to account for retransmissions in the schedule. We use analytic models of radio propagation to predict the number of retransmissions needed to achieve the desired probability of receiving a packet. Then, the schedule is generated by solving the scheduling constraints by using a Satisfiability Modulo Theory (SMT) solver. We verify the correctness of the resulting schedule to show that our constraints can produce a correct schedule. The performance of the schedule synthesis with different network sizes, topologies, and the number of transmissions are evaluated.