Supervisor

Suitable for

Abstract

Radio frequency identification (RFID) is used for object identification with application to devices connected to the Internet of Things. RFID protocols can benefit from formal verification techniques, and particularly quantitative verification with which a number of cost measures can be analysed. Recently, a Markov model was developed for performance analysis (“Performance Analysis of RFID Protocols: CDMA Versus the Standard EPC Gen-2”, IEEE Transactions on Automation Science and Engineering, vol.11, no.4, pp.1250-1261, 2014). The idea is to develop a parametric PRISM model (www.prismmodelchecker.org) based on this Markov model and analyse its energy usage characteristics. The advantage of the parametric model is that it can be used to automatically determine optimal parameter values that guarantee that a given property is satisfied. The PRISM model of the ZigBee protocol (http://www.prismmodelchecker.org/casestudies/zigbee.php) may be useful for this purpose. This project would suit a student interested in probabilistic modelling and Internet of Things.