# A Rule-Based Language and Verification Framework of Dynamic Service Composition
## 3 Declarative Formalism for the Service Composition
### A Formal Syntax and Semantic of the Service Composition Language: GSLang
#### 3.2.2 Service and Service Instance  
A **service** is defined by a unique identifier, output variables (output parameters), input variables (input parameters), post-conditions, guards and a location. A service can depend on other services.  
\[\begin{array}{rcl}S&::=&id(\;\overline{\overline{x}},\overline{\mathrm{e_{b }}}^{x}\;)\;(\overline{\overline{y}},\overline{\mathrm{e_{b}}}^{y}\;)\;[ \alpha]\mid\\ &&id(\;\overline{\overline{x}},\overline{\mathrm{e_{b}}}^{x}\;)\;(\overline{ \overline{y}},\overline{\mathrm{e_{b}}}^{y}\;)\;[\alpha]\to\mathrm{S_{1}}... \mathrm{S_{n}}\end{array}\]  
A service is elementary or composite. It is characterized by output parameters \(\overline{\overline{y}}\), input parameters \(\overline{\overline{x}}\), possibly the effects on the output parameters \(\overline{\mathrm{e_{b}}}^{y}\), possibly preconditions on input parameters \(\overline{\mathrm{e_{b}}}^{x}\) and an identifier (its name). It can be composed of other services \(\mathrm{S_{1}}...\mathrm{S_{n}}\). \(\alpha\) represents the location of service. It should be noted that \(\alpha\) may be unnecessary for services on the RHS if they are implemented in the same user space as the services from the LHS.  
For reasons of readability, we prefer the previous notation. In pi-calculus notation, it corresponds to:  
\[\begin{array}{rcl}S&::=&[\overline{\mathrm{e_{b}}}^{x}\;]\;\alpha\;(id, \overline{\overline{x}},p)\;.\;[\overline{\mathrm{e_{b}}}^{y}\;]\;p\overline{ \overline{y}}\;\mid\\ &&[\overline{\mathrm{e_{b}}}^{x}\;]\;\alpha\;(id,\overline{\overline{x}},p)\;. (\cdot p_{1}\;\alpha\;(id_{1},\overline{\overline{x}}_{1},p_{1})\;\mid\\...\;\mid\;S_{i}...\;\mid\;\;vp_{n}\;\alpha\;(id_{n},\overline{\overline{x}}_{ n},p_{n})\;.\;[\overline{\mathrm{e_{b}}}^{y}\;]\;p\overline{\overline{y}}\end{array}\]  
The S service expects \(\overline{\overline{x}}\) as the parameter, executes and returns \(\overline{\overline{y}}\). It receives the data on the public port of the peer where it is hosted. when the RHS is present, it calls the services it contains to build \(y\). The services on the RHS can be executed in parallel if the data are independent of each other or in sequence if there is dependency hence the parallel operator(\(\mid\)) inside the brackets in bold. Once a call of service performed, we get the service instances. These notations are also used to describe the instances.  
The **Service instance** or **Artifact** is the instantiation of a service. This makes it possible to follow the execution of the service.  
\[I ::= id(\;\overline{\overline{x}},\overline{\overline{e}_{\mathrm{b}}}^{x}) (\;\overline{\overline{y}},\overline{\overline{e}_{\mathrm{b}}}^{y})\;[\alpha]\;|\] \[id(\;\overline{\overline{x}}_{r},\overline{\overline{e}_{\mathrm{b} }}^{x})\;(\;\overline{\overline{y}},\overline{\overline{e}_{\mathrm{b}}}^{y})\;[ \alpha]\;|\] \[id(\;\overline{\overline{x}}_{r},\overline{\overline{e}_{\mathrm{b} }}^{x})\;(\;\overline{\overline{y}},\overline{\overline{e}_{\mathrm{b}}}^{y})\;[ \alpha]\;|\] \[id(\;\overline{\overline{x}}_{r},\overline{\overline{e}_{\mathrm{b} }}^{x})\;(\;\overline{\overline{y}},\overline{\overline{e}_{\mathrm{b}}}^{y})\;[ \alpha]\to\mathrm{I}_{1}...\mathrm{I}_{n}\;|\] \[id(\;\overline{\overline{x}}_{r},\overline{\overline{e}_{\mathrm{b }}}^{x})\;(\;\overline{\overline{y}},\overline{\overline{e}_{\mathrm{b}}}^{y})\;[ \alpha]\to\mathrm{I}_{1}...\mathrm{I}_{n}\;|\] \[id(\;\overline{\overline{x}}_{r},\overline{\overline{e}_{\mathrm{b }}}^{x})\;(\;\overline{\overline{y}}_{r},\overline{\overline{e}_{\mathrm{b}}}^{y}) \;[\alpha]\to\mathrm{I}_{1}...\mathrm{I}_{n}\;\]  
A service instance has several configurations:  
* the input and the output parameters are not yet resolved;
* resolved input parameters and output parameters not yet resolved;
* resolved input and output parameters.  
Each element that appears on the right, when it exists, can have one of the three previous configurations. The parameters of the service instances are resolved as they are executed.