# An Actor-Based Formal Model and Runtime Environment for Resource-Bounded IoT Services +
## 4 Operational Semantics  
This section presents the operational semantics for the proposed model. We define the state of an IoT service as follows:  
**Definition 2** (Service State).: _A service is denoted as \(s\) and is written as:_  
\[[\![I:\ \alpha:\ O]\!]_{s} \tag{1}\]  
_where \(s\) is the service's unique name, \(I\) is a set of input ports of the service, \(\alpha\) is a set of agents of the service, and \(O\) is a set of output ports of the service._  
Here, we are only interested in modeling the interactions between services, so we do not show data messages with local recipients within a service. As agents are modeled as actors, \(\alpha\) can be considered as an actor map which maps a finite set of actor addresses to their behaviors. A coordinator actor of a service \(s\), written as \(a_{s}\in\alpha\), receives all messages sent to \(s\). Note that there is a one-to-one mapping between \(s\) and \(a_{s}\) (i.e., for each service \(s\), there is exactly one coordinator agent).  
Figure 2: Communication between services.  
**Definition 3** (Model Configuration).: _The instantaneous snapshot of a system of services is called a service model configuration. This configuration represents the state of a finite set of long-lived IoT services, a finite set of contracts between services which define how services are connected to each other, and a finite set of control messages between services. A contract is negotiated between two services when one of them wants to consume service feeds produced by the other._  
The model configuration can be represented by a 3-tuple:  
\[\langle S\mid C\mid M\rangle \tag{2}\]  
\(S\) is a set of services. \(C\) is the set of contracts between the services, where each contract \(c\in C\) has the form \((s_{1},\ s_{2},\ map)\), where \(s_{1}\) is the name of the first service, \(s_{2}\) is the name of the second service, and \(map\) is a name table which says which output ports of the first service are connected to which input ports of the second service. The connections are represented using \((o\ ;\ i)\) pairs where \(o\in O\) is an output port of \(s_{1}\) and \(i\in I\) is an input port of \(s_{2}\). The contracts involving a service \(s\in S\) can be written as \(co(s)\subset C\). \(M\) is a finite set of control (inter-service) messages in the system which are communicated between services and are handled by coordinator actors of the communicating services.  
Our model assumes that there is a special service, called the _directory service_, which has up-to-date information about the capabilities of all contributing IoT services in the system. For example, the service capability of a sensor service is determined by the maximum sampling rate of that sensor. The directory service fits the service definition (Definition 1) because it has non-empty finite sets of input ports, output ports and agents. The directory service can be implemented as a federated hierarchy of directory services, which can be distinguished by different metrics such as geographical locations, type of services, etc. Each contributing service in the system must be registered with the directory service in order to participate in serving client services. Note that the names and capabilities of all contributing services registered with the directory service are all part of the directory service's state.