The development of the Internet of Things (IoT) came with the manufacturing of a huge amount of smart things equipped with sensors for making them aware of their environment, and with network connection for allowing remote interaction with them. However, most smart things still lack enough autonomy and context-awareness, hindering them from being people-friendly and actually useful for their users' everyday tasks. IoT devices should take advantage of their sensors and smartness to react automatically to the needs of their users and to provide seamless interactions with them. Within this field, the authors work on the design of Digital Avatars, a mobile computing framework for dynamically programming interactions among smart devices. The framework is based on the virtual profile of the user, which is inferred, stored, and shared by their smartphone. The profile provides a personalized context for running scripts which interact with IoT devices. This way, smartphones become a digital avatar of the user, capable of acting as a personal and seamless interface with their IoT environment. In this work, we present a formalization of Digital Avatars by means of a Linda-based approach with multiple shared tuple spaces. By means of a case study, we show how properties of the systems can be proved, and we briefly describe an implementation of both the Digital Avatars framework and the case study.
