Model verification in foraging behavior of swarm robotics using SPIN model checker / Nur Atiqah Ibrahim

Swarm robotics systems normally consist of many homogeneous robots that operate autonomously without a global controller. It is inspired by swarms of insects cooperating to deliver food items that a single individual cannot move. An example of foraging behavior is in ant colonies that represent of how complex group behavior can arise from simple individuals. In the aspect of industrial and scientific settings, collaboration between robots and humans is crucial and increasingly as a compliment to human nowadays. Therefore, it is very significant for developing of robots in the industry development of robot helpers for more general use such as in the workplace, at home, and in health-care environments. However, before such robots can be fully utilized, a comprehensive analysis of their safety is necessary to check their deadlock and any violations occurred. Unfortunately, in real environment, these processes or activities have not been verified using model checker approach. Some researchers have studied and come out with the model based on PFSM of foraging behavior of swarm robotics. In short, their proposed process, activities or states model did not undergo a rigorous analysis based on model checking technique, hence the results could subject to failure or malfunction. Therefore, we have used formal verification in which one can verify the system and automatically checks whether a model meets its given specification. In this research, we apply a swarm robotics in food foraging problem in order to carry out the foraging task. The aim is to model foraging behavior in PROMELA code in order to verify their correctness properties in term of their safety by using SPIN model checker to avoid counterexample. The result of model checking then has been extended in order to be able to detect violations that occur in the model and also verify it by using assertion and never claim correctness properties. According to the result, it has been proved that SPIN model checker can be used to check the deadlock, counterexample and any violations occurred in the system in term of their safety and trustworthy. Hence, it is useful for software engineers to solve the problem the failure of software or malfunction in the system.