Formal verification of RFID system using model verification agent

Radio Frequency Identification (RFID) technology has brought about revolutionary changes to software system development that supports major applications in advanced business and asset management. Over the years, many RFID applications have been implemented and integrated into the existing system esp...

詳細記述

書誌詳細
第一著者: Lockman, Muhammad Tarmizi
フォーマット: 学位論文
言語:英語
出版事項: 2012
主題:
オンライン・アクセス:http://eprints.utm.my/10042/1/MuhammadTarmiziMFSKSM2012.pdf
_version_ 1846215325692985344
author Lockman, Muhammad Tarmizi
author_facet Lockman, Muhammad Tarmizi
author_sort Lockman, Muhammad Tarmizi
description Radio Frequency Identification (RFID) technology has brought about revolutionary changes to software system development that supports major applications in advanced business and asset management. Over the years, many RFID applications have been implemented and integrated into the existing system especially in asset management. When the number of RFID devices and system connected to the existing system increases, the network traffic will be overloaded and congested. This would cause problems in reading the RFID tags and could reduce the effectiveness of the existing system in operation. Although many researches have been done on the RFID system, research on formal verification of RFID system has not yet been fully explored. In this thesis, the architecture of a Model Verification Agent (MVA) is presented to verify the processes involved in the RFID utilizations based on the properties of format, syntax and slot of time. In comparison to conventional techniques such as testing and simulation of tracking errors, this thesis proposes a MVA approach to formalize the RFID processes in RFID system. The architecture of MVA is applied on the case study of RFID applications using the MVA to support the verification process. The formal specification language of MVA is designed using Linear Temporal Logic (LTL) and this is supported by the Communication Sequence Processes (CSP) in Concurrency Workbench of New Century (CWB-NC) tool. Two case studies have been used to validate the proposed model; RFID embedded smart card and RFID shopping system. Specifications in the MVA have proven to improve the efficiency of the RFID process based on the properties of the specified RFID system. Finally, the use of MVA has demonstrated that the approach is able to identify errors in the specifications of the RFID system design. This research will assist developers to find errors and improve the implementation of RFID based system developments for various applications.
format Thesis
id uthm-10042
institution Universiti Teknologi Malaysia
language English
publishDate 2012
record_format eprints
spelling uthm-100422018-05-27T03:19:47Z http://eprints.utm.my/10042/ Formal verification of RFID system using model verification agent Lockman, Muhammad Tarmizi QA Mathematics Radio Frequency Identification (RFID) technology has brought about revolutionary changes to software system development that supports major applications in advanced business and asset management. Over the years, many RFID applications have been implemented and integrated into the existing system especially in asset management. When the number of RFID devices and system connected to the existing system increases, the network traffic will be overloaded and congested. This would cause problems in reading the RFID tags and could reduce the effectiveness of the existing system in operation. Although many researches have been done on the RFID system, research on formal verification of RFID system has not yet been fully explored. In this thesis, the architecture of a Model Verification Agent (MVA) is presented to verify the processes involved in the RFID utilizations based on the properties of format, syntax and slot of time. In comparison to conventional techniques such as testing and simulation of tracking errors, this thesis proposes a MVA approach to formalize the RFID processes in RFID system. The architecture of MVA is applied on the case study of RFID applications using the MVA to support the verification process. The formal specification language of MVA is designed using Linear Temporal Logic (LTL) and this is supported by the Communication Sequence Processes (CSP) in Concurrency Workbench of New Century (CWB-NC) tool. Two case studies have been used to validate the proposed model; RFID embedded smart card and RFID shopping system. Specifications in the MVA have proven to improve the efficiency of the RFID process based on the properties of the specified RFID system. Finally, the use of MVA has demonstrated that the approach is able to identify errors in the specifications of the RFID system design. This research will assist developers to find errors and improve the implementation of RFID based system developments for various applications. 2012-01 Thesis NonPeerReviewed application/pdf en http://eprints.utm.my/10042/1/MuhammadTarmiziMFSKSM2012.pdf Lockman, Muhammad Tarmizi (2012) Formal verification of RFID system using model verification agent. Masters thesis, Universiti Teknologi Malaysia, Faculty of Computer Science and Information Systems.
spellingShingle QA Mathematics
Lockman, Muhammad Tarmizi
Formal verification of RFID system using model verification agent
title Formal verification of RFID system using model verification agent
title_full Formal verification of RFID system using model verification agent
title_fullStr Formal verification of RFID system using model verification agent
title_full_unstemmed Formal verification of RFID system using model verification agent
title_short Formal verification of RFID system using model verification agent
title_sort formal verification of rfid system using model verification agent
topic QA Mathematics
url http://eprints.utm.my/10042/1/MuhammadTarmiziMFSKSM2012.pdf
url-record http://eprints.utm.my/10042/
work_keys_str_mv AT lockmanmuhammadtarmizi formalverificationofrfidsystemusingmodelverificationagent