Abstract
An object locator is a device designed to assist its user in finding misplaced household and personal objects in a home. This thesis describes alternative designs and a proof-of-concept prototype of object locators based on the RFID technology. Advantages of such locators include extensibility, reusability and low maintenance. The numeric model provided here can be used to determine figures of merits, including costs, search time and energy consumption. The results of analysis based on the model can serve as design guides. This thesis also describes a parser that translates state diagrams into a model checking language. The parser is useful to developers who want to formally verify designs specified by state diagrams.