# A Rule-Based Language and Verification Framework of Dynamic Service Composition
## 1 Introduction  
Services are increasingly developed and published on the Web. Often, these services taken alone serve lightweight functionality. In many cases, a single service is not sufficient to satisfy user requests. So several services need to be combined to achieve a specific goal [1; 2]. Several languages were proposed to define composite services. These languages rely for the most part on process models with the BPML language as the reference [2]. The latter provides structured and rigid blocks based on graphs which are then translated into static composite services. The ability to manage the flexibility and the evolution of a composite service at runtime is an essential requirement. For example, a user in order to prepare its travel, needs to buy a flight ticket and reserve a room. The user get in touch with a travel agent which will communicate with a hotel service and an airline service. May be the travel agent make available the possibility to rent a car. This new service can be provided by a car rent service or one of the initial agent (hotel or airline). The new service will be added in the travel agent space without stop the running service. In addition, the car rent service is optional for the users who need it. The changes in travel agent requirements have an immediate impact on the specification of the composite services. This situation can occur even at runtime since the services which participate to a composite can be removed or added any time. Therefore, the need to have the flexible and adaptive services composition approach is a necessity. Several studies have been carried out to make them more adaptable during execution [1; 2; 3; 4; 5]. To this end, it is appropriate to offer languages that promote more flexibility (as soon as the services are specified) and adaptability (in the execution framework). To meet these requirements, rule-based declarative approaches were proposed because they promote reusability, adaptability and flexibility for the composition of services [7]. How can we take into account the user needs or the new services even during the execution of a composite service? The research question in this paper deals with the proposition of a language for the definition of flexible and adaptable services. Rather than providing runtime techniques to adapt to the changes [3], the required need consists of anticipating the changes by relying on a language which is purely declarative and rules oriented which facilitates a greater flexibility and adaptation by describing the execution schema of the composition (the _what_) rather than the execution path of the composition (the _how_). The proposed language here is based on the production rules with the purpose to operationalize the Guarded Attributed Grammar (GAG) model [8] through the specification of a service composition language. Basically, GAG models are designed principally in order to contribute to the modelling of artifact-driven workflows. They are declarative rules-based, data-oriented, user-centric, and distributed. The transposition of all these properties in the domain of the services composition makes it possible to have a more flexible composition environment because the language proposed in this article is purely declarative and based on the rules. A composite service is defined by using grammar productions as composition rules. The left hand side of a production rule defines a new service that is obtained by assembling the entities on the right hand side. Any change in the description of the composition scheme is automatically taken into account when the affected rule is applied. The services are connected at runtime through the dependencies between their attributes. The composition is controlled by the data and the associated conditions so-called guards. The operational semantics which consists of a description of the services selection, the creation of the instances of the services and their refinements is presented using process algebra (pi-calculus) [9].