| Summary: | <p> The application of mobile robots has been increased in recent years to include search-and-rescue where a set of robots sweep an area searching for an item of interest, patrolling where a set of robots patrol a fence to protect a region, and pattern formation where the robots form a given pattern. Cooperative mobile robots are autonomous entities that are able to self-coordinate their actions in order to solve a global task, such as emergency response, in distributed systems. In order to achieve the desired cooperation, mobile robots are required to be synchronized. Existing synchronization algorithms need external information from an outside source, depend on a reliable network where messages cannot be lost or corrupted, or require a fixed number of mobile robots during the execution. These are disadvantages in practical applications because messages can simply be lost due to noise or interference in the communication channel. Moreover, the number of mobile robots may vary due to unforeseen incidents such as hardware or software malfunctions. </p><p> In order to address the aforementioned problems, a synchronization algorithm with failure detection has been proposed, implemented, and verified. The proposed algorithm guarantees when all robots start their current assigned task within a bounded time, then the time interval in which they will start the next given task will be bounded as well. The simulation results show that the robots are still able to start the given task in the next round synchronously if the number of consecutive lost messages is less than four. </p><p> The proposed model was developed using the SPIN model checker. The safety and liveness properties were defined using the Linear Time Logic (LTL) in order to verify its functionality under error-prone conditions. It was shown that the proposed algorithm gave the correct results.</p><p>
|
|---|
