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

Full description

Saved in:

Bibliographic Details
Main Author:	Lockman, Muhammad Tarmizi
Format:	Thesis
Language:	English
Published:	2012
Subjects:	QA Mathematics
Online Access:	http://eprints.utm.my/id/eprint/10042/1/MuhammadTarmiziMFSKSM2012.pdf
Tags:	Add Tag No Tags, Be the first to tag this record!

id	my-utm-ep.10042
record_format	uketd_dc
spelling	my-utm-ep.100422018-05-27T03:19:47Z Formal verification of RFID system using model verification agent 2012-01 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 http://eprints.utm.my/id/eprint/10042/ http://eprints.utm.my/id/eprint/10042/1/MuhammadTarmiziMFSKSM2012.pdf application/pdf en public masters Universiti Teknologi Malaysia, Faculty of Computer Science and Information Systems Faculty of Computer Science and Information Systems
institution	Universiti Teknologi Malaysia
collection	UTM Institutional Repository
language	English
topic	QA Mathematics
spellingShingle	QA Mathematics Lockman, Muhammad Tarmizi Formal verification of RFID system using model verification agent
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
qualification_level	Master's degree
author	Lockman, Muhammad Tarmizi
author_facet	Lockman, Muhammad Tarmizi
author_sort	Lockman, Muhammad Tarmizi
title	Formal verification of RFID system using model verification agent
title_short	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_sort	formal verification of rfid system using model verification agent
granting_institution	Universiti Teknologi Malaysia, Faculty of Computer Science and Information Systems
granting_department	Faculty of Computer Science and Information Systems
publishDate	2012
url	http://eprints.utm.my/id/eprint/10042/1/MuhammadTarmiziMFSKSM2012.pdf
_version_	1747814788147183616

Formal verification of RFID system using model verification agent

Similar Items