Modelling and analysis of energy usage for RFID protocols
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.