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 ch...

Full description

Saved in:

Bibliographic Details
Main Author:	Ali, Siti Shafinaz
Format:	Thesis
Language:	English
Published:	2015
Subjects:	Programming Rule-based programming Backtrack programming
Online Access:	https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf
Tags:	Add Tag No Tags, Be the first to tag this record!

id	my-uitm-ir.107735
record_format	uketd_dc
spelling	my-uitm-ir.1077352024-12-16T06:50:56Z Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali 2015 Ali, Siti Shafinaz Programming. Rule-based programming. Backtrack programming Robotics. Robots. Manipulators (Mechanism) 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. 2015 Thesis https://ir.uitm.edu.my/id/eprint/107735/ https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf text en public masters Universiti Teknologi MARA (UiTM) Faculty of Computer and Mathematical Sciences Abdul Basit, Kamarul Ariffin
institution	Universiti Teknologi MARA
collection	UiTM Institutional Repository
language	English
advisor	Abdul Basit, Kamarul Ariffin
topic	Programming Rule-based programming Backtrack programming Programming Rule-based programming Backtrack programming
spellingShingle	Programming Rule-based programming Backtrack programming Programming Rule-based programming Backtrack programming Ali, Siti Shafinaz Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
description	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.
format	Thesis
qualification_level	Master's degree
author	Ali, Siti Shafinaz
author_facet	Ali, Siti Shafinaz
author_sort	Ali, Siti Shafinaz
title	Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
title_short	Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
title_full	Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
title_fullStr	Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
title_full_unstemmed	Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali
title_sort	verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / siti shafinaz ali
granting_institution	Universiti Teknologi MARA (UiTM)
granting_department	Faculty of Computer and Mathematical Sciences
publishDate	2015
url	https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf
_version_	1818588231170523136

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

Similar Items