# A Rule-Based Language and Verification Framework of Dynamic Service Composition
## 3 Declarative Formalism for the Service Composition
### Basic Definition  
A service is defined within the frame of an activity. An activity is a tuple  
\[\text{A}=(id,S,C)\]  
where  
* **Id** is a unique identifier of the activity (for example, its name);
* **S** is the execution schema that describes the services \(\{t_{0},t_{1}...t_{n}\}\) to be performed to resolve the activity;  
Where the inputs of the RHS depends on the inputs of the RHS of other services, the outputs of the RHS and the inputs of LHS of s. The outputs of the LHS are functions of the outputs of the RHS. \(f\) materializes this dependency Example:  
\[\begin{array}{l}travelService(username,date,destination)\langle numVol, hotelAdress \rangle\rightarrow\\.\quad flightBooking(username,date,destination)\langle numVol\rangle\\.\quad hotelReservation(username,date)\ \langle hotelAdress\rangle\end{array}\]  
\(numVol\) of \(travelService\) corresponds to \(numVol\) to \(flightBooking\). Other examples can be taken for this \(travelService\) service.  
The semantic rules are also expressed by the conditions on the input and the output parameters which serve as guards and post-conditions.  
This so-called intentional definition is materialized during its instantiation. The service instance takes place according to the availability of the data (parameters). When the composition scheme of an activity is updated, the modification will be applied next time the associated rule be enacted. The semantic rules may involve several variables which belong to different peers. At this moment a private dynamic channel is opened for the interaction between the peers. These are the reasons why the pi-calculus is chosen in the next section to specify the composition language. In fact, one can notice that calculi based on the pi calculus provide primitives for describing and analyzing global distributed infrastructure, focusing on process migration between peers, process interactions via dynamic channels, and private channel communication [9]. In the process algebra (pi-calculus) [9], the processes execute actions that can have three forms: the sending of a message over x channel (written \(\overline{x}\) ), the receiving of a message over x channel (written \(x\)), and silent actions (written \(\tau\)), whose details are unobservable. Send and receive actions are called actions of synchronization, since communication is highlighted when the processes synchronize. The transition notion represents the executing a process expression. Intuitively, the transition relation indicates how to perform one-step of the process execution. Note that since there may be many ways to execute a process, the transition is basically non-deterministic. The transition of a process A into a process B by performing an action \(\alpha\) is indicated A \(\stackrel{{\alpha}}{{\longrightarrow}}\) B. The action \(\alpha\) is the observation of the transition.  
The description of the services thus defined and their behaviors are based on primitives of instantiation, refinement and exchange of messages which can also be found in more abstract languages such as process algebras. This permits us to describe the structure of a service and present formally how a service is defined and how it interacts in its environment. In the following, we describe formally the syntax and the semantics of a service composition language.