# From Service Composition to Mashup Editor: A Multiperspective Taxonomy
## 4 Taxonomy for Services Composition
### System Perspective
#### 4.1.1 Formal Approach  
Formal models can be used for the automatic or manual modeling of composed services. The formal description techniques allow for the use of methods and tools to make the development cycle of services more reliable, faster, and cheaper. Formalisms for specifying these services are based on precise and mathematically based syntaxes and semantics. Developing models will apply methods and tools in three major phases of the development lifecycle of the service: (i) the verification, (ii) the automatic or semi-automatic code generation, and (iii) the generation of the test benches.  
The objective of the verification phase is to improve the reliability of the process of developing an implementation by ensuring that the formal model on which the implementation is based is valid with respect to a given set of properties. These properties are represented in the form of logical properties or sub-sets of an automaton [20; 21].  
The formal test phase is a set of executions of specific test sequences on the implementation. Test sequences are obtained from the formal model by trying to cover all aspects of the service compound. Tests can be generated automatically or semi-automatically based on criteria, goals, or assumptions. There are many stages and types of tests in the development process of a service: the conformance, the interoperability, the unit test, and the integration tests. The majority of these procedures are standardized or described in some reference software development lifecycle management [22].  
Depending on the degree of modeling, it is possible to generate code for all or part of the application model. The more precise the semantics modeling language, the more complete the code generation. For instance, in the UML formalism, semantics are weakor nonexistent. At best, they will generate the interfaces from the model. Many modeling languages have been standardized and are based on various concepts such as automata, the states/transitions systems, temporal logic, interaction, etc. [23]. Some of them are briefly described in the following.  
The Specification and Description Language (SDL)  
SDL [24] is a specification language standard defined by the International Telecommunication Union (ITU-T), which aims to describe communication protocols. Even if the SDL is a modeling language that was initially used for communication protocols description, it is more generally used for modeling real-time applications. This is due to the syntax of the language, which describes a service using the following:  
* Description in the form of state machines;
* Exchange of information via asynchronous messages;
* Use of timers.  
The ECharts Formalism  
The ECharts is a state machine-based programming language that was developed by ATT Laboratories and was first introduced in 1999. It is still actively supported today due to its textual and graphical syntax. The goal of ECharts is to provide an easy way to describe modular, verifiable, maintainable, and reusable services and composite services. ECharts is based on a state machine formalism, which allows for the modeling of transitions with priorities (event-driven systems). This feature provides flexibility in reusing models from a given machine, as new transitions can be added to certain states with a higher priority than the existing transitions, thus modifying the behavior of the original machine [25].  
In summary, this approach offers formal methods to verify or test software components (services) automatically, which are necessary for the composition of services. However, these formalisms are too specific and require high technical and mathematical skills, and therefore cannot be directly used by end-users, but can intervene at underlying layers to ensure some required properties (such as security properties).