# An Actor-Based Formal Model and Runtime Environment for Resource-Bounded IoT Services +
## 5 The Proximity Model
### Properties and Propositions
If the sensed data is a result of aggregating multiple sensing feeds, then \(d_{\zeta}\) becomes the maximum time delay between the oldest feed and the delivery time of the aggregate._  
Contributor tuples are created using a function \(f_{\Xi}\) as follows:  
\[f_{\Xi}(\rho_{i},S_{\rho_{i}})\rightarrow\Xi_{\rho_{i}}=\{\xi_{1},\ldots,\xi_ {k}\} \tag{14}\]  
where \(\Xi_{\rho_{i}}\) denotes the set of all contributor tuples which are sufficient to serve \(\rho_{i}\), \(S_{\rho_{i}}\) is the set of contributors who collectively participate in serving \(\rho_{i}\), \(\xi_{i}\) is a single contributor tuple generated from a contributor \(s_{i}\), and \(k\) is the size of the \(\Xi_{\rho_{i}}\) set. A contributor tuple \(\xi_{i}\) is represented as follows:  
\[\xi_{i}=\langle s,si,\tau,d_{\zeta},\omega\rangle \tag{15}\]  
where \(s\) denotes a contributing service's unique name (i.e., actor name), \(si\) represents the sensing instructions, \(\tau\) is the sensing time, \(d_{\zeta}\) is the maximum time delay between the sensing time and sending data to the service coordinator, and \(\omega\) represents the sensing data. Note that \(\omega\) is empty before filling the sensing data by the contributor service. The following transition rule shows the process of assigning the sensing tasks represented in the contributor tuples \(\Xi_{\rho_{i}}\) to \(S_{\rho_{i}}\):  
\[ \begin{split}\langle[\![I:&[R[multicast(S_{\rho_{i}}, \Xi_{\rho_{i}})]]\!]_{a_{d_{\zeta}}},\,\alpha\,:\,O\!]_{s_{d}},\,S\mid C\mid M\rangle \\ &\rightarrow\langle[\![I:&[R[nil]]_{s_{d}}\,,\, \alpha\,:\,O\!]_{s_{d}},\,S\mid C\mid\langle S_{\rho_{i}}\Leftarrow M_{\Xi} \rangle,\,M\rangle\end{split}  \tag{16}\]  
where \(s_{d}\) is a directory service; \(S_{\rho_{i}}\) is a set of contributing services which will participate in serving \(\rho_{i}\), \(\Xi_{\rho_{i}}\) is the set of the contributor tuples (i.e., sensing tasks); \(M_{\Xi}\) is a set of actormessages where each \(m\in M_{\Xi}\) is a message sent to \(s_{j}\in S_{\rho_{i}}\), where \(m=\langle s_{j}\Leftarrow\Xi_{s_{j}}\rangle\); and \(\Xi_{s_{j}}\subset\Xi_{\rho_{i}}\) such that \(\Xi_{s_{j}}\) is \(s_{j}\)'s sensing assignment. On receiving its assigned set of contributor tuples \(\Xi_{c}\), a contributor \(c\) adds them to its schedule, as follows:  
\[ \begin{split}\langle s\mid\{(\textit{receive})_{c},C\}\mid \Theta\mid P\lvert m,\mu\rvert t\rangle\rightarrow\\ \langle s\mid[\textit{add\_to schedule}(\Xi_{c},st)_{c} ]_{c},C\mid\Theta\mid P\mid\mu\rvert t\rangle\end{split}  \tag{17}\]  
where \(m=\langle c\Leftarrow\Xi_{c}\rangle\) is a schedule message, \(\Xi_{c}\) is the contributor tuples assigned to contributor \(c\), and \(st_{c}\) is the contributor's state. Each contributor \(c\) senses/executes the tuples that have a sensing time equals to \(t\). After the sensing computation in \(\xi_{\tau}\) is executed, \(d\) is filled in with the sensing data, and a serve-next message is sent to the contributor itself in order to serve the next message or sensing task. The contributor then sends the sensed data \(d\) to the server when \(t\geq\tau+\delta\), as described by the following transition rule:  
\[ \begin{split}\langle[I:[\textit{sense}(\xi)]_{a},\alpha:\mu:O]_{ s_{1}},S\lvert C\lvert\mu\rvert t\rangle\rightarrow\\ \langle[I:(\textit{receive})_{a},\alpha:\mu:\mu:O]_{s_{1}},S \lvert C\lvert m,\mu\rvert t\rangle\end{split}  \tag{18}\]  
where \(s_{1}\) is a contributing service, \(s_{2}\) is a consuming service, \(\xi=\langle s_{2},si,\tau,d_{\xi},nil\rangle\), \(\xi^{\prime}=\langle s_{2},si,\tau,d_{\xi},\omega\rangle\), and \(m=\langle s_{2}\Leftarrow\omega\rangle\) is a data contribution message. On receiving a contribution message \(m=\langle s\Leftarrow\omega\rangle\), the server actor proceeds to aggregate the message and update the request's state, as follows:  
\[