1. UPPAAL
2. Oracle BPEL Process Manager
1. Oracle JDevelper Studio Edition
2. Oracle Application Server
3. Oracle BPEL Control

The adopted hardware environment is characterized by:
- Windows XP Service Pack 3 operating system,
- 2 GB of disk space, a minimum of 2 GB RAM and a minimum of 1535 MB of swap space.

In this section, we describe the tools used for the realization of our conformance testing approach: UPPAAL and Oracle BPEL Process Manager.

1. UPPAAL

Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems which are modelled as networks of timed automata, extended with data types. The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark.
A Timed Automaton is a finite-state machine extended with clock variables. It uses a dense-time model where a clock variable evaluates to a real number. All the clocks progress synchronously. In Uppaal, a system is modelled as a network of several such timed automata in parallel. These automata communicate by binary synchronization using syntax like transmission/reception. Thus, on a channel c, a transmitter sends the signal c! and a receiver synchronizes with it by the additional signal c?.
A state of the system is defined by the locations of all automata, the clock values, and the values of the discrete variables. It may have a condition on clocks called invariant that must be satisfied for the duration spent in this state. Every automaton may fire an edge (sometimes misleadingly called a transition) separately or synchronize with another automaton1, which leads to a new state. A transition is labelled by:
- Guard: A guard label expresses a condition on the value of variables or clocks. It must be met to pass the transition,
- Synchronization: A synchronization label is either on the form Expression! or Expression? or is an empty label,
- Update: An update label expresses the reset of some clocks and the update of some integer variables.
The graphical interface (GUI) of Uppaal is divided into three main parts: the editor, the simulator, and the verifier, accessible via three “tabs”.
- Editor: the editor is used to model a system with timed automata.
- Simulator: the simulator is used to study the function and properties of a modelled system and to predict its evolution and detect modelling errors.
It can be used in three ways: the user can run the system manually and choose which transitions to take, the random mode can be toggled to let the system run on its own, or the user can go through a trace (saved or imported from the verifier) to see how certain states are reachable.
- Verifier: the verifier is designed to test certain types of properties of a formal specification such as:


* Non-blocking property: it expresses that the system is never in a situation where it cannot progress.
* Accessibility property or safety of a model: it expresses an event under certain conditions can never occur.
* Liveness property: it expresses an event under certain conditions will eventually occur.
We use UPPAAL to model, validate and verify Timed Automata specifying Web service compositions. UPPAAL also generates an XML file describing this specification. In our work, we use the structure of this XML file for the realization of tests.

2. Oracle BPEL Process Manager
Oracle BPEL Process Manager provides a framework for designing, deploying and managing BPEL processes. It can work in the context of a service-oriented architecture and make use of its various technologies like XML, SOAP and WSDL. It processes the different types of activities of a BPEL process like basic, structured and communication activities. It is multi-platform and can be integrated with different application servers such as WebLogic, Oracle Application Server. The following figure shows the architecture of Oracle BPEL Process Manager and its components.
Oracle BPEL Process Manager
1. Oracle JDevelper Studio Edition
Oracle JDeveloper is an integrated development environment for building applications and Web services using Java technologies, XML and SQL standards. Using a palette that contains the various activities of a BPEL process, it allows designing a BPEL process and integrating it with its services partners. Oracle JDeveloper is used to deploy the developed processes directly to Oracle BPEL Server.

2. Oracle Application Server
Once the BPEL process is compiled and modelled, it can be deployed. The deployment phase is to send the JAR Project to Oracle Application Server that validates this archive.

3. Oracle BPEL Control
If the compilation and deployment are successful, Oracle BPEL Control can execute, monitor and manage BPEL processes designed and deployed with Oracle JDeveloper.