# An Actor-Based Formal Model and Runtime Environment for Resource-Bounded IoT Services +
## 5 The Proximity Model
### Properties and Propositions  
The necessary and sufficient condition for serving an IoT service request is stated in Axiom 2, as follows:  
**Axiom 2: Serving a service request. ** A service request set to \(\rho_{i}\in\rho\) can be served by a set of contributors \(C_{\rho_{i}}\in C\) if and only if each member of \(\rho_{i}\) can be served by a subset of \(C_{\rho_{i}}\). The necessary and sufficient condition for serving a client tuple is stated in Axiom 3, as follows:  
**Axiom 3: Serving a client tuple. ** A client tuple \(\zeta\in\rho_{i}\) can be served by a set of contributors \(C_{\zeta}\) if and only if \(C_{\zeta}\) has the sensing capabilities to serve the requirements of \(\zeta\), and \(\zeta\) can be accommodated in \(C_{\zeta}\)'s sensing schedules. There are two types of deadlines set by the directory service in each contributor's request to serve \(\rho_{i}\): (i) the offer response's deadline by which a contributor has to respond to the directory service's request; and (ii) the offer acceptance's deadline by which the directory service has to accept the contributor's response to its request. The following axiom describes the conditional contributor commitment to contribute in serving the service request:  
**Axiom 4: Conditional contributor commitment. ** A contributor \(c\in C_{\rho_{i}}\) conditionally commits to serving its part, \(Z^{c}_{\rho}\in\rho\), if it indicates its capability to serve \(Z^{c}_{\rho}\) to the directory service, and \(Z^{c}_{\rho}\) can be accommodated in \(c\)'s sensing schedule, with the condition that the directory service accepts the assignment of \(Z^{c}_{\rho}\) to \(c\) by a deadline \(d_{Z^{c}_{\rho}}\). We assume that the directory service guarantees to send a confirmation message to the contributor service before the deadline \(d_{Z^{c}_{\rho_{i}}}\) if the directory service has accepted \(c\)'s offer. The following axiom describes the unconditional contributor commitment to contribute in serving the service request:  
**Axiom 5: Unconditional contributor commitment. ** A contributor \(c\)'s conditional commitment to serve \(Z^{c}_{\rho_{i}}\) becomes unconditional when the server accepts \(c\)'s offer by the deadline \(d_{Z^{c}_{\rho_{i}}}\). Theorem 3.1: _If the directory service accepts a request \(\rho\), it is served._  
Proof: According to Axiom 1, if a request \(\rho\) is accepted in the system, there must be at least one set \(\rho_{i}\in\rho\) which can be served by the directory service, and the service can schedule the processing time required to serve \(\rho_{i}\). According to Axioms 2 and 5, if \(\rho_{i}\) can be served by the directory service, the directory service must have received unconditional offers from a set of contributors \(C_{\rho_{i}}\in C\) to participate in serving \(\rho_{i}\). To obtain an unconditional commitment from a contributor \(c\in C_{\rho_{i}}\), according to Axiom 4, \(c\) must have checked its sensing schedule and temporarily reserved a time slot for serving its part in \(\rho_{i}\). \(c\) would have sent an offer to the server by the deadline, and this offer would have been accepted by the server by \(c\)'s deadline. The directory service would have sent a confirmation message to \(c\). Then, \(c\) would have, finally, sent a message to the directory service conforming that \(c\) has scheduled its part in \(\rho_{i}\) for execution. If all members in \(C_{\rho_{i}}\) have sent a confirmation message to the directory service, this means each member \(c\in C_{\rho_{i}}\) must have scheduled its part, \(Z^{c}_{\rho_{i}}\in\rho_{i}\), for execution. In other words, \(C_{\rho_{i}}\) has unconditionally committed to collectively serve a set of client tuples \(Z_{\rho_{i}}\) which covers all members in \(\rho_{i}\). Therefore, \(\rho\) has a commitment to be served by both a set of contributors and the directory service. This means that a request \(\rho\) is served if the directory service accepts it, which proves Theorem 3.1.