# An Actor-Based Formal Model and Runtime Environment for Resource-Bounded IoT Services +
## 5 The Proximity Model
### Fine-Grained Resource Model for IoT Services
in a system of services by a resource term \(\epsilon=[r,l_{r}]_{\tau}^{\lambda}\), where:  
* \(\langle r,l_{r}\rangle\) denotes the located type of the specified resource. It contains both the type of the resource \(r\) and the relative location (locality) of the resource \(l_{r}\). The locality could be relative or absolute based on the type of the service. Note that the location where the resource is residing is dynamic, as we deal with mobile resources. * \(\lambda\) represents the rate of availability of the resource, in quantity or time. For example, if the specified resource is a contributor's sensor, then this parameter represents the sampling rate of that sensor which is the time between any two consecutive context samplings. The higher its value, the more frequent the context is sampled. In addition, this parameter adjusts the required accuracy when sampling the context. The higher its value, the more precise the sampled context is. * \(\tau\) is the time interval during which the resource exists, where \(\tau=\langle t_{start},t_{end}\rangle\)  
For example, consider that a GPS sensor at a contributor is sampled at rate 10 Hz and available at a time interval \(\langle 0,5\rangle\), and can be represented as \([GPS,l_{GPS}]_{\langle 0,5\rangle}^{10}\). As each resource term is associated with a time interval \(\tau\), relationships between time intervals must be defined before we can discuss the operations on resource terms. We use interval algebra to formalize relations between two time intervals, as shown in Figure 3.  
If two resource terms in a resource set have the same located types and overlapping time intervals, they can be combined as follows:  
\[\epsilon_{1}\cup\epsilon_{2}=[r,l]_{\tau_{1}}^{\lambda_{1}}\cup[r,l_{r}]_{\tau _{2}}^{\lambda_{2}}=\{[r,l]_{\tau_{1}\backslash\tau_{2}}^{\lambda_{1}},[r,l]_ {\tau_{2}\backslash\tau_{1}}^{\lambda_{2}},[r,l]_{\tau_{2}\cap\tau_{1}}^{ \lambda_{2}+\lambda_{2}}\} \tag{27}\]  
where for any interval for which they overlap, their rates are added, and for remaining intervals, they are represented separately in the set, and \(\backslash\) is a relative complement operation. Figure 3: Possible relations between two time intervals. **Resource requirements of service requests:** A service request consumes resources at every step of its execution. We represent request's computations in terms of the resources they consume. Request's computations in our model can be divided into three categories: sensing computation at a contributor device, CPU processing at the server side, and network utilization. We represent the resource requirements for a contributor tuple \(\xi\) as follows:  
\[[R]^{(s,d)}_{\xi}=\Phi(\xi,s,d),R=\{r_{1},\ldots,r_{n}\},r_{i}=[q]_{\langle r, t\rangle} \tag{28}\]  
where \(\Phi\) is a function which takes a contributor tuple \(\xi\) as a parameter and returns a set of resource amounts representing the required resources for serving that tuple, \(s\) is the earliest start time of executing \(\xi\) (i.e., sensing time), \(d\) is the deadline by which the sensing task must be completed, and \(q\) is the quantity of resource required. For example:  
\[ \begin{split}\Phi(\xi,5,8)=[R]^{(5,8)}_{\xi}=[&\{[ 20k]_{\langle CPUJL_{C}PU\rangle},[100]_{\langle GPSJ_{G}PS\rangle}\\ &,[1k]_{\langle AccJ_{Acc}\rangle},[100 ms]_{\langle netJ_{net} \rangle}]^{(5,8)}\end{split}  \tag{29}\]  
Consider a function \(f\), which, when a resource set \(E\) and the resource requirement of a contributor tuple \([R]^{(s,d)}_{\xi}\) are provided as parameters, returns a Boolean value true or false, indicating whether or not the contributor tuple can be served given the available set of resources:  
\[f(E,\Phi(\xi,s,d))=(\bigcup_{s}^{d}E\geq\Phi(\xi))=true|false \tag{30}\]  
where \(\bigcup_{s}^{d}E\) gives the union of all resources in \(E=\{\epsilon_{1},\ldots,\epsilon_{n}\}\) which exist in the interval \((s,d)\). For each member \(r\) in \(R\), \(f\) searches in the set of available resources \(E\) for the amount of resources required to service \(r\).