Transformational Design of Business Processes in BPEL Language

A transformational approach to the design of executable processes in Business Process Execution Language (BPEL) is presented. It has been built upon the transformations of business processes accompanied by a formal approach based on process algebras used to verify the behavioral equivalence of business processes. The initial business process can be denoted in BPEL, then a series of transformations is executed upon it. The process resulting from the transformation is verified whether it preserves behaviour denoted by the process being transformed. The transformations improve non-functional properties of the process (performance, modifiability, granularity, maintainability) but do not change its original behaviour. The transformations are steered by Architecture Trade-off Analysis Method (ATAM) that shows the direction of changes and helps an architect to decide which of them to apply. An example of the application of our approach in real-life business process design has also been presented. The paper presents general idea of the design process, theoretical basis of the method as well as experimental verification of the approach and a tool implemented to support the method.