A Formal Programming Framework for Digital Avatars

A Formal Programming Framework for Digital Avatars? Alejandro P´erez-Vereda, Carlos Canal, and Ernesto Pimentel University of Malaga, Spain [email protected],[email protected],[email protected] Abstract. In the current IoT era, the number of smart things to interact with is raising everyday. However, each one of them precises a manual and specific configuration. In a more people-friendly scenario, smart things should adapt automatically to the preferences of their users. In this field, we have participated in the design of People as a Service, a mobile computing reference architecture which endows the smartphone with the capability of inferring and sharing a virtual profile of its owner. Currently, we are developing Digital Avatars, a framework for programming interactions between smartphones and other devices. This way, the smartphone becomes a personalized and seamless interface between people and their IoT environment, configuring the smart things with information from the virtual profile. In this work, we present a formalization of Digital Avatars by means of a Linda-based system with multiple shared tuple spaces. Keywords: Digital Avatars, People as a Service, PeaaS, Linda, Shared Tuple Spaces. 1 Introduction The Internet of Things (IoT) is built over a layer of connected devices and sensors that offer specific interfaces to access the information they collect and also to configure how they work, e.g. the frequency to pick up the data or how to format them [ 9 ]. Recent research in the IoT field has promoted the development of devices and sensors which are more configurable and provide easier interfaces. They are known as smart things [ 11 ]. However, smart things still require a lot of manual configuration, and this problem becomes more challenging the bigger the number of devices we daily interact with. In a desirable scenario, the technology should work for the people and not the other way around. Every smart thing should adapt to the needs of the people seamlessly and in an automatic way, reducing the need for interaction with the users to the minimum. Considering the pervasive presence of smartphones, the authors of this paper have participated in the design of a mobile computing reference architecture ? This work has been funded by the Spanish Government under grants PGC2018094905-B-I00 and TIN2015-67083-R (MINECO/FEDER). called People as a Service (PeaaS) [ 10 ]. This architecture promotes the use of smartphones to learn about their users, creating and storing virtual profiles with their preferences and context information. These profiles are then offered as a service to third parties in a secure manner. This way, smartphones become seamless and automatic interfaces that negotiate their owner’s preferences, adapting and configuring the smart things in their surroundings. For that purpose, the required interactions are not just simple data transfers, but we need mechanisms that allow to configure smart things, and also to complete virtual profiles with context knowledge obtained from these interactions. The more complete virtual profiles are, the better may the technology adapt to the people. With this goal in mind, we are developing Digital Avatars, a dynamic programming framework which allows defining the interactions between smartphones and smart things by means of on-the-fly scripts [ 13 ]. The scripts are executed in the smartphone, and they make use of the virtual profile stored in it for reconfiguring the behavior of the smart thing with the information available. Our programming framework is inspired by the vision of a Programmable World [ 17 ], which foresees the evolution from today’s IoT based on data recollection to truly programmable devices. This way, both smart things and smartphones are able to learn from each other, and to evolve through each interaction in a transparent and dynamic way. In this paper, we present a formal framework for Digital Avatars. The framework provides a formal description of virtual profiles and the scripts to execute on them, and it establishes the basis for issues like privacy or security, with secure connections controlling the access to virtual profiles. The formalization is based on a multiple shared tuple spaces model inspired by Linda, which makes possible to ensure the soundness of the framework, and makes feasible the analysis of some interesting properties. The rest of this paper is structured as follows. In Section 2 we present the motivations of this paper and discuss some related works. Next, Section 3 defines the concepts necessary to reason on Digital Avatars. In Section 4, we formalize the interactions that take place in the framework and demonstrate interesting formal properties of the system. Then, Section 5 presents a proof of concept and analyze its implementation using the framework. Finally, Section 6 draws the conclusions of the paper and briefly discusses future work. 2 Background The development of smart things is transforming people’s lives, as we increasingly interact with them everyday. Social Computing (SC) [ 18 ] is the area of computer science that deals with the interaction between social behavior and computer systems. SC encompasses all those systems that collect, process and disseminate information related to individuals and groups of people. The goal is learning about people and their preferences and providing an easy adaptation of their IoT environment, reducing manual configuration of devices to a minimum. Indeed, a number of recent research works agree on giving support to the IoT by means of a paradigm focused on people [16]. Currently, very few companies are able to access and process this enormous quantity of social information, and to exploit and make a profit from it. In practice, this reduces the SC marketplace to a small number of big stakeholders. As Tim Berners-Lee declared recently [ 1 ], SC systems should empower people, making them the fair owners of their information, and deciding who has access to it. Moreover, this information must be stored in a unique and accessible place which lets third parties use it in a controlled way, following the privacy preferences of the users. In this same sense, we advocate for developing collaborative architectures based on smartphones. Their pervasive presence in people’s everyday lives and their increasing sensoring and computing capabilities, together with their communication skills, make them key elements for obtaining, processing, and sharing information about their users [ 15 ]. Smartphones are also the most appropriate devices to be in charge of negotiating the interactions of their users with smart things in their environment. Architectures based on P2P models are gradually acquiring a greater presence in fields such as social networks [ 19 ] or recommendation systems [ 20 ]. The basis of these architectures are the virtual profiles of the users, plenty of contextual data (e.g. activities, relations with other users, etc.) [ 8 ]. Our goal is sharing these virtual profiles with third parties and to adapt the IoT environment to the preferences and needs of each user. With that purpose in mind, our approach is based on a Linda-like model. Linda [ 7 ] is a coordination language where synchronization is achieved by means of a shared tuple space, and through a set of simple but enough expressive primitives [ 2 ]. However, a single shared tuple space would violate the principles of the PeaaS model. Some other Linda-like proposals have been made by different authors, introducing some kind of mobility, mainly based on adding capabilities for remotely modifying a given tuple space. Thus, Lime [ 14 ] was proposed as a Linda extension to support mobile computing, by the definition of transiently shared distributed tuple spaces to establish P2P communications. Some of its goals are common with ours, but our framework also takes into account privacy issues, which are crucial for virtual profiles. Another well-known proposal is KLAIM [ 5 ], which extends Linda by considering the possibility of remote adding tuples to an accessible tuple space. With a similar philosophy, SCEL [ 6 ] was designed to provide a parametric language to capture various programming abstractions for autonomic components and their interaction. In both cases, Linda-like primitives were added to allow the remote interaction with shared tuple spaces. Although the PeaaS paradigm could be (artificially) coded by these languages, a number of assumptions and constraints should be made to ensure the main PeaaS features. In fact, we consider that accessing to a virtual profile has to be made only by its owner, and remote accessing to transient tuple spaces or shared repositories do not model these scenarios properly. 3 Modeling Digital Avatars In order to define a formal framework for reasoning on Digital Avatars, we introduce the notion of virtual profile together with a number of related concepts, and we describe how virtual profiles can be offered as services under the PeaaS paradigm. 3.1 Definitions The key issue for taking into account the user in an IoT environment is her virtual profile. It contains information about user preferences, habits, movements, or relations. All this information is only stored in the user’s device (e.g. a smartphone), and it is offered as a service to third parties. The definition below formalizes this notion. Definition 1. Avirtual profile P is a multiset of entities, where each entity is a 5-tuple t = ( n, s, p, v, ts )composed of (i) n∈Name representing the name of the entity, (ii) s∈Type defines the entity’s type, (iii) p∈Privacy , which provides the level of privacy, (iv) v∈Value is the value of the entity itself, with a structure which will depend on the entity’s type, and (v) a timestamp ts ∈T ime , which allows recording the time when the tuple is added to the virtual profile. We will denote by Tthe set of tuples, and by Pthe set of virtual profiles. The complexity of virtual profiles depends on the sets Name , Type , Privacy , Value , and Time . These entities are structured in nested sections for the secure and correct functioning of the profile. Although the model does not depend on how these particular domains are defined, we consider a common minimum structure for predefined entities which are characterized as follows: Personal It consists in personal and contact information of the user ( personal ∈ Name ); the default privacy is private ∈Privacy , although it can be overwritten in each attribute to allow accessing it to family or friends, for instance. Basically, it contains a collection of entity identifiers like name , phone , address, or email with the corresponding information. Relations It provides information on how users are related to each other ( relation ∈ Name ), such that values includes entity names like family , friends , colleagues , or acquaintances . These nested entities are collections of user (personal) information with information about location, social profiles and their certificate hash fingerprint. The default privacy level of these entities is private ∈ Privacy. Places It defines information in a profile concerning locations ( place ∈Name ): home, place of work, known places or other places. Thus, constants like home or work belong to the Name set in the value of this entity. Their default privacy level is trusted. A virtual profile can be accessed and/or modified by means of processes executing appropriate actions. In order to formalize this idea, we are inspired by Linda [ 4 ], a coordination language [ 7 ] consisting of a set of inter-agent communication primitives, which can be virtually added to any programming language. Primitives in Linda allow processes to read, delete, and add tuples in a shared tuple space. Tuple spaces are a convenient approach to represent virtual profiles shared by concurrently running processes. A virtual profile is represented by a multiset of tuples encapsulated in a device. Thus, we adopt a multiple tuple space model. Following other approaches [ 3 , 12 ], we shall consider a process algebra L including the Linda communication primitives and the usual concurrency connectives, parallel and non-deterministic choice. The primitives permit to add a tuple (out), to remove a tuple (in), and to check the presence (or absence) of a tuple (rd, nrd) in a given profile (tuple space). Processes in L provide a convenient way to model scripts which can be downloaded from a server and run on a smart device. Thus, the syntax of L is formally defined as follows: S∈ L ::= 0 |α.S |S+S|SkS|S(˜ t) α∈Act ::= rd(t)|nrd(t)|in(t)|out(d, t) where 0 denotes the empty process, d∈D a device identifier, and t denotes a tuple. The process S ( ˜ t ) denotes a procedure call where the procedure definition will be given by a script template S ( ˜x ) (where ˜x is a sequence of variables instantiated by a sequence of tuples ˜ t ). In order to simplify the definition of rules modelling the L primitive actions in Subsection 4.2, we will assume that reading a tuple do not imply the evaluation of usual operations (e.g. arithmetic operations) nor the variable instantiation as usual in Linda-based languages. This assumption does not imply any loss of generality of the proposal. Notice that we consider primitives for locally accessing, adding, and removing tuples to a tuple space (i.e. a virtual profile). Although we could have also considered accessing and deleting tuples from remote tuple spaces, for our purposes we only need to add tuples remotely. For this reason, only the out primitive includes as a parameter the device on which adding the tuple. That is, rd , in and nrd actions will be made locally, on the same device where the script is being run. The same considerations were made in [ 12 ]. As it will be shown later, remote adding of tuples will only affect to the artifact where the script was downloaded from, thus we will not allow arbitrary remote adding of tuples. This asymmetric treatment of out and read primitives are precisely one of the features devoted by the PeaaS model: local accessing is only made by device owners, and remote changes can only be made on artifacts providing the scripts to be run. In our framework, we distinguish two kinds of artifacts: smart devices and smart things. The difference between them is that smart devices exhibit computing capabilities, and therefore they can download and execute scripts, whereas smart things only provide a (link to a) script. Formally, we define an artifact as a pair consisting of a virtual profile and a process corresponding to the execution of one or several scripts. We assume that D is a set of artifact identifiers. Every artifact d also has associated a script definition Sd ( ˜x ) which can be downloaded by other artifacts with computing capabilities (i.e. smart devices). Definition 2. An artifact d∈D is characterized by a pair hP : Sid , including a virtual profile P and a process S∈ L , corresponding to the running scripts on the artifact. In addition, an artifact can contain a script definition Sd ( ˜x ). We will denote by Sd ( P )the script instantiated by the specific tuples in the profile P . And we will represent by D=P × L × Dthe set of artifacts. A smart thing will be characterized by having only a profile; that is, its process is always the empty process 0. A typical example of smart thing would be a beacon broadcasting a Bluetooth Low Energy (BLE) signal which encodes the URL of a script file to be downloaded from a server. On the other hand, typical smart devices are smartphones, tablets, or any other device with computing capabilities. Both kinds of artifacts —smart things and smart devices— store information in a virtual profile. 3.2 Security in Digital Avatars The actions executed over the virtual profile of a smart device may emerge from internal processes of the device, or they may be part of a script downloaded from another artifact (e.g. a beacon broadcasting a link to a script file) when several conditions are fulfilled: the smart device is close enough to the beacon, the beacon artifact is registered, its script code is trusted, etc. In order to avoid running untrusted scripts, we assume a Certification Authority capable to ensure the trustfulness of an artifact d , and a Boolean mapping certify which provides this information in such a way that certify ( d ) is true when the emitter of dhas been authenticated. In addition, the out primitive considered in the previous section allows adding tuples to both local and remote virtual profiles. Although the model imposes no limitations on which profiles can be remotely modified, the artifact identifier d used in a remote out(d,t) in a script Sd ( ˜x ) can only be that of the artifact d itself. Thus, an artifact’s profile may only be remotely modified by running a script downloaded from this same artifact. Hence, in order to guarantee that the actions executed while running a script on a smart device are secure, we assume a Boolean mapping accept : Act × P → {true,false} that restricts which primitives are enabled, in such a way that accept(α, P ) is true when the action αis acceptable on the profile P. However, using certificates and restricting remote addition of tuples is not enough to ensure a correct interaction between source and target artifacts, and we also need to consider some technical issues. Indeed, whereas certify provides a third-party declaration about the trust of an artifact, and accept controls what actions are permitted inside an artifact once the script has been downloaded, we need a way to detect when two artifacts are actually able to communicate with each other. For instance, consider a scenario where a smartphone (represented by a virtual profile P ) approaches a smart thing d which provides a script Sd ( ˜x ). For downloading the script from d and running it in the smartphone, we assume a mapping links : P ×D→ 2 T , which provides a link to connect to the smart thing, depending on the availability to download, the closeness between both artifacts, good signal strength, etc. This mapping returns a set of tuples representing links (e.g., a URI or a bluetooth connection) providing a way to access the artifact d . If there are no links, or the profile P does not accept downloading the script offered by d,links(P, d) will be the empty set. Notice that all the notions introduced in this subsection (accept,certify, and links) are application specific, in such a way that their particular definitions will depend on the application domain and context where our framework is applied to. 4 Formal framework Now that we have defined the main elements and concepts of our framework, we can formalize the interactions between artifacts by means of a transition system with in-device and remote operations. Then, we show how some interesting properties like bisimilarity and congruence are accomplished by the model. 4.1 In-device transition system The operational semantics of L is modeled by the following labelled transition system: · −→⊆ D × Λ× D defined by the rules 1 of Table 1, where D = P × L × D and Λ = {t, t, t : t∈ T}∪{τ}. Rule Out 1 describes how the output operation proceeds as an internal move (represented by label τ ) which adds the tuple t to the profile P (comma is used to represent the multiset union). Rule Out 2 shows that a tuple t is ready to offer itself to the artifact/device by performing an action labelled t . Rules In and Read describe the behavior of the prefixes in ( t ) and rd ( t ) whose labels are t and t , respectively. Rule NRead describes the prefix action nrd ( t ), which proceeds when t is not in the profile P ; the transition is labelled with ¬t . All these rules need that the current device’s profile accepts the corresponding action. It is worth noting that we do not include any kind of evaluation nor variable instantiation when reading tuples, as it is usually made in Linda-related transition rules. This is only for simplicity reasons without loss of generality. Rule Sum is the standard rule for choice composition. Rule Sync 1 is the standard rule for the synchronization between the complementary actions t and t . It models the effective execution of an rd ( t ) operation. Notice that the resulting profile is left unchanged, since the read operation rd ( t ) does not modify it. Rule Sync 2 defines the synchronization between two processes performing transitions labelled with t and t , respectively. It models the effective execution of in ( t ) 1For the sake of simplicity we will consider only finite processes here. action. The usual rule Par 1 for the parallel operator can be applied to any label. The transition system is considered closed w.r.t. commutative and associative properties for sum (+) and parallel (k) operators. (Out1)accept(out(d, t), P ) hP:out(d, t).Sid τ −→ hP, t :Sid (Out2)hP, t :Sid ¯ t −→ hP:Sid (Read)accept(rd(t), P ) hP:rd(t).Sid t −→ hP:Sid (In)accept(in(t), P ) hP:in(t).Sid t −→ hP:Sid (NRead)t6∈ P∧accept(nrd(t), P ) hP:nrd(t).Sid ¬t −→ hP:Sid (Sum)hP:S1id α −→ hP0:S0 1id hP:S1+S2id α −→ hP0:S0 1+S2id (Sync1)hP:S1id t −→ hP:S0 1idhP:S2id t −→ hP0:S2id hP:S1kS2id τ −→ hP:S0 1kS2id (Sync2)hP:S1id t −→ hP:S0 1idhP:S2id t −→ hP0:S2id hP:S1kS2id τ −→ hP0:S0 1kS2id (Par1)hP:S1id α −→ hP0:S0 1id hP:S1kS2id α −→ hP0:S0 1kS2id Table 1. Transition system for smart devices Notice that action out ( d, t ) is only considered in Table 1 when it is running in the device d . Its full behavior (remote adding of tuples) will be defined when the interaction among devices is expressed in Table 2. 4.2 Remote transition system In order to define how artifacts interact, we consider configurations composed of a parallel composition of artifacts as follows: hP1:S1id1| hP2:S2id2| · · · | hPn:Snidn where Pi ( i = 1 ..n ) are virtual profiles of artifacts —either smart devices and smart things—, Si are scripts running in smart devices, and di represent the device identifiers. Notice that we denote in a different way the parallel composition of artifacts ( | ) and the parallel composition of processes inside a smart device ( k ). The transition system · −→ defined in Table 1 is extended to configurations by the inference rules given in Table 2. (Remote)accept(out(e, t), Q) hP:out(e, t).Sid| hQ:Tie τ −→ hP:Sid| hQ, t :Tie (Sync3)certify(e)∧b∈links(P, e) hP:Sid| hQ:Tie τ −→ hP, b :SkSe(b, Q)id| hQ:Tie (Par2)D1 α −→ D0 1 D1|D2 α −→ D0 1|D2 Table 2. Transition system Rule Remote models remote actions modifying the virtual profile which belongs to the smart thing from which the script being run was downloaded. We consider this transition as a silent step from an observational point of view. For this reason, we use the label τ. Rule Sync 3 represents the interaction between two artifacts (typically, a smart device and a smart thing). In this case, the script associated with a smart thing e , previously certified, is downloaded through a link b establishing a connection between the virtual profile P and e . Thus, the script to be executed in the context of the smart device d (in parallel with other possible pending processes) will be Se ( b, Q ) (such as it was defined in Definition 2). Notice that, in this case, the script is instantiated not only by the profile Q but also by the link b . This allows customizing the script to the artifact which provides access to it. In addition, the link tuple b is added to the profile P , so recording that the smart thing has been already “visited”. Rule Par 2 describes the way in which the parallel composition of artifacts proceeds. Note that the parallel composition of processes inside a smart device is modelled by Rule Par 1 in Table 1. Actually, any interaction in the context of a smart device is governed by rules in that table. We consider the transition system closed w.r.t. usual structural congruence (commutative and associative properties) of both parallel connectors. The rules in Table 1 and Table 2 are used to define the set of derivations in an environment where smart devices and smart things are interacting with each other. Following [ 3 ], both reductions labelled τ and reductions labelled ¬t are considered. Formally, this corresponds to introducing the following derivation 3. Nadia Busi, Roberto Gorrieri, and Gianluigi Zavattaro. On the Turing equivalence of Linda coordination primitives. Electr. Notes Theor. Comput. Sci., 7:75, 1997. 4. Nicholas Carriero and David Gelernter. Linda in context. Commun. ACM, 32(4):444– 458, April 1989. 5. R. De Nicola, G. L. Ferrari, and R. Pugliese. Klaim: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering, 24(5):315– 330, May 1998. 6. Rocco De Nicola, Diego Latella, Alberto Lluch Lafuente, Michele Loreti, Andrea Margheri, Mieke Massink, Andrea Morichetta, Rosario Pugliese, Francesco Tiezzi, and Andrea Vandin. The SCEL Language: Design, Implementation, Verification, pages 3–71. Springer International Publishing, Cham, 2015. 7. David Gelernter and Nicholas Carriero. Coordination languages and their significance. Commun. ACM, 35(2):96–, February 1992. 8. Tor-Morten Grønli, Gheorghita Ghinea, and Muhammad Younas. Context-aware and automatic configuration of mobile devices in cloud-enabled ubiquitous computing. Personal and ubiquitous computing, 18(4):883–894, 2014. 9. Jayavardhana Gubbi, Rajkumar Buyya, Slaven Marusic, and Marimuthu Palaniswami. Internet of Things (IoT): A vision, architectural elements, and future directions. Future generation computer systems, 29(7):1645–1660, 2013. 10. Joaquin Guillen, Javier Miranda, Javier Berrocal, Jose Garcia-Alonso, Juan Manuel Murillo, and Carlos Canal. People as a Service: a mobile-centric model for providing collective sociological profiles. IEEE software, 31(2):48–53, 2014. 11. Dominique Guinard, Vlad Trifa, Friedemann Mattern, and Erik Wilde. From the Internet of Things to the Web of Things: Resource-oriented architecture and best practices. In Architecting the Internet of Things, pages 97–129. Springer, 2011. 12. Ronaldo Menezes, Andrea Omicini, and Mirko Viroli. On the semantics of coordination models for distributed systems: The LogOp case study. In Foundations of Coordination Languages and Software Architecture (FOCLASA 2003), volume 97 of Electronic Notes in Theoretical Computer Science, pages 97–124. Elsevier, 2004. 13. Alejandro P´erez-Vereda, Daniel Flores-Mart´ın, Carlos Canal, and Juan M Murillo. Towards dynamically programmable devices using beacons. In International Conference on Web Engineering, volume 11153 of LNCS, pages 49–58. Springer, 2018. 14. Gian Pietro Picco, Amy L. Murphy, and Gruia-Catalin Roman. Lime: Linda meets mobility. In Proceedings of the 21st International Conference on Software Engineering, ICSE ’99, pages 368–377. ACM, 1999. 15. Mika Raento, Antti Oulasvirta, and Nathan Eagle. Smartphones: An emerging tool for social scientists. Sociological methods & research, 37(3):426–454, 2009. 16. Jorge Sa Silva, Pei Zhang, Trevor Pering, Fernando Boavida, Takahiro Hara, and Nicolas C Liebau. People-centric Internet of Things. IEEE Communications Magazine, 55(2):18–19, 2017. 17. Antero Taivalsaari and Tommi Mikkonen. A roadmap to the programmable world: software challenges in the IoT era. IEEE Software, 34(1):72–80, 2017. 18. Fei-Yue Wang, Kathleen M Carley, Daniel Zeng, and Wenji Mao. Social computing: From social informatics to social intelligence. IEEE Intelligent systems, 22(2), 2007. 19. Yufeng Wang, Athanasios V. Vasilakos, Qun Jin, and Jianhua Ma. Survey on mobile social networking in proximity (MSNP): approaches, challenges and architecture. Wireless networks, 20(6):1295–1311, 2014. 20. Wan-Shiou Yang and San-Yih Hwang. iTravel: A recommender system in mobile peer-to-peer environment. Journal of Systems and Software, 86(1):12–20, 2013.