Cover Image

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
Robotics. Robots. Manipulators (Mechanism)
Online Access:https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf
https://ir.uitm.edu.my/id/eprint/107735/
Tags: Add Tag
No Tags, Be the first to tag this record!
id my.uitm.ir.107735
record_format eprints
spelling my.uitm.ir.1077352024-12-16T06:50:56Z https://ir.uitm.edu.my/id/eprint/107735/ Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali 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 NonPeerReviewed text en https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf Verification of correctness properties for aggregation behavior of swarm robotics system using spin model checker / Siti Shafinaz Ali. (2015) Masters thesis, thesis, Universiti Teknologi MARA (UiTM). <http://terminalib.uitm.edu.my/107735.pdf>
institution Universiti Teknologi Mara
building Tun Abdul Razak Library
collection Institutional Repository
continent Asia
country Malaysia
content_provider Universiti Teknologi Mara
content_source UiTM Institutional Repository
url_provider http://ir.uitm.edu.my/
language English
topic Programming. Rule-based programming. Backtrack programming
Robotics. Robots. Manipulators (Mechanism)
spellingShingle Programming. Rule-based programming. Backtrack programming
Robotics. Robots. Manipulators (Mechanism)
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
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
publishDate 2015
url https://ir.uitm.edu.my/id/eprint/107735/1/107735.pdf
https://ir.uitm.edu.my/id/eprint/107735/
_version_ 1818838388614103040
score 13.239859

Similar Items