# A Rule-Based Language and Verification Framework of Dynamic Service Composition
## 3 Declarative Formalism for the Service Composition
### Service Resolution  
The operational semantics defined above consist in creating and materialize the service instances dynamically at runtime according to the input and output parameters and the port created during execution. In the system a service instance I is resolved if all these parameters are defined (input and output). Any action on a resolved service does not change it. i.e.,  
I is resolved \(\iff I^{*}\)  
The semantics of this operator are as follows: if \(I^{*}\) and I \(\stackrel{{ a}}{{\longrightarrow}}I^{\prime}\) then \(I^{\prime*}\). **Theorem 1**. : _A service instance I to which are attached the input variables \(\overline{\overline{x}}\) and the output variables \(\overline{\overline{y}}\) is resolved if all the associated service instances \(I_{i}\) are resolved i.e.,_  
\[\frac{I\to I_{1}...I_{n},\ I_{1}^{*},\ I_{2}^{*}...,\ I_{n}^{*}}{I^{*}}\]  
**Proof. ** If the instance is simple i.e., it is defined by \(I\rightarrow\), then \(I\) is resolved if the values are assigned to the input parameters \(x_{r}\) and the output parameters \(y_{r}\). If the instance is composite i.e., \(I\to I_{1}...I_{n}\)  
* A instance like \(I\to I_{1}\), by definition, \(x\subseteq x_{1}\) and \(y\subseteq y_{1}\) if \(I_{1}\) is resolved i.e. we have \(x_{r1}\) and \(y_{r1}\) then x and y are defined i.e. \(x_{r}\) and \(y_{r}\). * A instance like \(I\to I_{1}...I_{n}\) by definition, The input (resp. output) variables of the LHS x (resp. y) depends on the input (resp. the output) parameters of the RHS: \(x\subseteq\cup_{i}x_{i}\) (resp. \(y\subseteq\cup_{i}y_{i}\)). if \(\forall_{i}I_{i}\) is resolved i.e. we have the \(x_{ir}\) and \(y_{ir}\), \(\Rightarrow\) we have \(x_{r}\) and \(y_{r}\). The operational semantics generate a \(\bot\)-transitions system. Proof. : Let a labeled \(\bot\)-transition system defined by a n-tuple \((\Sigma,S,\rightarrow,\bot)\) where  
* \(\Sigma\) is a set of **actions** which label the transitions;
* \(Q=S\cup I\) is the set of states where S is the set of **services** and I is the set of **instances**;
* \(\delta\subseteq Q*\Sigma*Q\) the transition function
* \(\bot\in S*bool\) is a termination predicate such that \(\bot\) (\(s\)) = _true_ and \(s\xrightarrow{\alpha}s\) then \(\bot\) (\(s\)) = _true_  
The transition system describes the behavior of a service when it is chosen in a user space. In Figure 1, all the operations of the operational semantics are used to describe how an instantiated service will progress to be solved. The operations convert the system from one state to another through attribute interpretation (silent action), sent and received messages. These latter correspond in the transition system to labelled edges. The services and the instances are the nodes. When we look at the instantiation rule C1, if the system containing a service of the form \(\mathrm{id}(\overline{\mathfrak{F}})(\overline{\mathfrak{F}})\) (node of the transition system) receives a message (\(\alpha(M,p)\)) (edge in the transition system) then the system creates an instance of the form \(id(\overline{\mathfrak{F}}_{r})(\overline{\mathfrak{F}})\). When the instance \(id(\overline{\mathfrak{F}}_{r})(\overline{\mathfrak{F}})\) is created, one can call the related service using the request \(vp_{i}\alpha(M,p_{i})\) (rule Req). The receiving of the response to this \(p_{i}(M)\) request (rule R2) allows refining the initial service thus defining the output \(id(\overline{\mathfrak{F}}_{r})(\overline{\mathfrak{F}}_{r})\). On the other hand, for a composite service, applying rule C2 when receiving a message on the public port of a peer \(\alpha(M,p)\), creates the instance with the values of the services of the LHS defined \((id_{0}(\overline{\mathfrak{F}}_{r})(y)\to I_{1}...I_{n})\). Therefore a refinement can be applied (rule R3) which allows through the semantic rules to define certain parameters of the RHS.