Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali

Swarm robotics is a new approach to the coordination of multi-robot systems which consist of large numbers of relatively simple robots (typically homogenous) which takes its inspiration from social insects. Referring previous research, the algorithm only focus on communication instead of rigorous checking. This research work focused on a developed swarm algorithm aimed at swarm aggregation. The main goal of this research is to verify the correctness properties of an existing model of aggregation behavior of swarm robotics. From the previous researcher, the aggregation algorithm based on the Probabilistic Finite State Automata (PFSA) is derived from the study of cockroach behavior. This algorithm is based on PFSA only relies on local interactions between individuals, the extensibility of the algorithm is very weak. In this research, we take inspiration from natural swarm and then transform to FSM. From FSM aggregation behavior algorithms is built for robot swarms. Model checking is a technique that was originally developed for verifying that finite state of the concurrent systems that implement specifications expressed in temporal logic. PROMELA language and verifying the proposed aggregation algorithm using the SPIN model checker. According to the result present in this research work, it has been proved that SPIN is capable to analyze the swarm robotic system using correctness properties. By verifying rigorously checking with SPIN model checker, the aggregation algorithm has been verified with no counter example and trustworthy.