| Sažetak | Web Service Business Process Execution Language (WS-BPEL) je dominantan standard za integraciju postojećih web usluga u cjelinu kojom se podupire izvršavanje poslovnog procesa. Cilj integracije nije samo omogućiti razmjenu poruka između učesnika poslovnog procesa, nego razmjenu poruka realizirati tako da se ona izvršava točno u trenutcima i na način kako bi se odvijali koraci stvarnog poslovnog procesa. WS-BPEL koristi na XML-u zasnovan jezik koji podržava web tehnologije. Budući da WS-BPEL specifikacija ne određuje službeni standard za vizualno modeliranje procesa, javila se ideja za razvojem vlastitog modela za vizualno modeliranje procesa. Osim vizualnog modeliranja, kao potrebna pokazala se formalna verifikacija izvršavanja budući da se unutar WS-BPEL procesa mogu pojaviti paralelna izvršavanja čime ponašanje sustava zbog brzine paralelnih komponenti postaje potencijalno nesigurno. Ovaj doktorski rad razradio je korake modela faznog modeliranja WS-BPEL poslovnog procesa na način da su ključne faze razvoja WS-BPEL procesa vezane za vizualno modeliranje i formalnu verifikaciju, a tu je i faza statičke provjere izvršnog modela procesa prema pravilima definiranim WS-BPEL specifikacijom. Za vizualno modeliranje predložen je standard Business Process Model and Notation (BPMN) koji je u pozadini također zasnovan na jeziku XML. Definiran je algoritam za dvosmjerno automatsko preslikavanje između standarda BPMN i WS-BPEL. Za prikazivanje formalnog modela odabrana je sintaksa Process Meta Language (Promela). Cilj formalne verifikacije je provjera rukovanja varijablama kao ključnim elementima poslovnog procesa. Osim predloženog faznog modela za razvoj WS-BPEL procesa i pripadajućih algoritama, u doktorskom radu je definiran i radni okvir s prijedlozima konkretnih alata koji su korišteni za realizaciju modela i pripadnih algoritama. Verifikacija algoritama korištenih u modelu i radnom okviru je izvršena nad hipotetičkim poslovnim procesima. |
| Sažetak (engleski) | Service-oriented architectures (SOA) represent the evolution of software development which has evolved after maturity of object-oriented architectures. Object-oriented architectures have introduced objects as reusable pieces of code while service-oriented architectures have moved one step further in the process of software reuse and have introduced possibilities of application reuse. Applications expose their functionalities as services in the standardized way (WSDL interfaces) and they can be integrated into more complex functionalities, i.e. business processes. Web Service Business Process Execution Language (WS-BPEL) is a predominant standard used for the integration of existing web services into executions used for the automation of business processes. WS-BPEL syntax is XML based and as already stated WS-BPEL processes communicate with WSDL services using SOAP protocol for communication. Services integrated into WS-BPEL processes are called partners and they are called when necessary. Process executions are similar to flow charts where partners are called when necessary. WS-BPEL standard offers a rich set of constructs, like conditional executions, event-driven executions, error handlings, compensation executions, and so on thus contained process behavior can become extremely complex. Since the WS-BPEL standard is based on XML syntax and no official standards nor approaches are offered for visual modeling of WS-BPEL processes, this resulted in an idea to develop a proprietary model that can be used for visual modeling of WS-BPEL processes which is one of the scientific contributions of the paper. Constructs offered by WS-BPEL specification can produce processes containing parallel executions which is a possible uncertainty in process execution because of the unpredictable execution speed of parallel components. The possibility of parallelism inside of WS-BPEL processes resulted in a need to develop formal methods that can check all possible executions of WS-BPEL processes. Formal checking presented in this dissertation is focused on the detection of parallel manipulation of process variables. WS-BPEL specification has defined a set of specific rules that must be verified by static analysis of the process before the process is deployed. This resulted in a need to develop an iii algorithm to automate static analysis of WS-BPEL processes which is the third algorithm of the scientific contribution of this dissertation. Algorithms and phases of WS-BPEL process development (visual modeling, formal verification, and static analysis) have resulted in the need to develop a model for phase development of WS-BPEL processes and a corresponding proposal for an implementation framework. Identified needs: algorithms for visual modeling, formal verification, and static analysis, as well as the model for phased development of WS-BPEL processes and its implementation framework, represent the scientific contributions of this dissertation. WS-BPEL standard is presented in chapter 2 where WS-BPEL offered constructs and related standards are introduced. In chapter 3 phased model for the development of WS-BPEL processes as one of the scientific contributions, is presented. Phases of the model integrate all the algorithms (visual modeling, formal verification, and static analysis) into the coherent whole. The first phase of the model is related to the visual development of the WS-BPEL process. Visual model, as output of the first phase, is transformed into WS-BPEL code and brought into the second phase where manual upgrade of the resulting WS-BPEL code is performed to make it executable. The third phase of the model is related to performing formal verification of the WS-BPEL code to find parallel variable manipulations or readings of uninitialized variables. If violations are found, correction of the WS-BPEL code is performed as a part of the fourth phase and the same cyclic process of formal verification and correction is performed until the resulting WS-BPEL code is satisfactory. The fifth and possibly the final phase of the model is related to the static analysis of the WS-BPEL code. Changed WS-BPEL code from any phase can be transformed into the visual model if changes affect the visual representation of the WS-BPEL process. Phases of the model are interconnected so the development of WS-BPEL processes is a complete process and it was the intention of the scientific contribution related to the model. When considering phased model development, it is assumed that the WS-BPEL process is made up of the existing web services, i.e. determining functionalities that will be exposed as web services is not part of the proposed phased model. It is a prerequisite that the services already exist before their integration into WS-BPEL processes is started. The first phase of the model presented in chapter 3 is related to visual modeling of processes while chapter 4 of the dissertation introduces standard used for visual modeling and bidirectional algorithm for transformation between visual and execution WS-BPEL model. iv Business Process Model and Notation (BPMN) standard is used for visual modeling of WS-BPEL processes because of its relation to business processes in general and because of its high level of standardization and a wide selection of offered BPMN tools. As part of chapter 4, BPMN executions (named as visual activities) are paired up with the corresponding WS-BPEL activities to show how they are visually presented in BPMN graphs. Since the BPMN standard is XML based as well as WS-BPEL standard, XML background code of visual activities and the XML code of the corresponding WS-BPEL activities are paired up. Functions for bidirectional transformations between XML BPMN graphs and XML WS-BPEL graphs are introduced. There is a gap between mechanisms of connecting elements inside of BPMN and WS-BPEL graphs. Sequence flows are used to connect sequential BPMN elements whilst WS-BPEL graphs are block-based. The difference between connection mechanisms was a challenge that had to be overridden when constructing bidirectional functions for transformations of sequence BPMN elements into populated WS-BPEL sequence activity and vice versa. Another challenge was the transformation of nested visual activities. Nesting to an arbitrary depth had to be supported by bidirectional transformation algorithms. BPEL flow activity was also a challenge since it can contain complex synchronized behavior. A proposal for visual modeling of BPEL flow activity was made but the transformation to XML code is left to be manual. The automatic bidirectional transformation of BPEL flow activity can be considered as a task for future work. Chapter 5 has introduced approaches for automatic static analysis of WS-BPEL code if chosen categories of rules are satisfied in the process. Automatic analysis can improve the development of WS-BPEL processes since its XML structure can be quite complex and manual static analysis can be error-prone. A static analysis of WS-BPEL processes is performed in the final phase of the proposed phased model for the development of WS-BPEL processes presented in chapter 3. Chapter 6 has introduced steps for the formal checking of WS-BPEL processes. Promela is used as a syntax for presenting formal models expressed as finite-state automata. Elements of WS-BPEL processes included in formal models are all parallel executions inside of processes as well as all behavior that performs variable manipulations. To generate Promela's formal models more efficiently, the generation of symbolic models based on source WS-BPEL processes is proposed. Symbolic models serve as transitions towards a successful generation of final formal models and they systematically list all elements of the WS-BPEL process (and their corresponding details) that are relevant for formal verification to transform them into the formal v model according to the predefined rules. Formal verification presented in this dissertation inspects if there are parallel variable writings and readings or attempts of using uninitialized or variables of inadequate types. If there are such violations in executions of the formal model, they are easily located in the symbolic model which helps to locate them more easily in the WS-BPEL process to correct its behavior. A scientific basis upon which formal verification of Promela code is performed is s synchronous product of finite-state automata. Checked WS-BPEL code, expressed as Promela code, is one finite-state automata (formed as an asynchronous interleaving product of parallel components of WS-BPEL process) and it is the first input into the synchronous product upon which verification is performed. The second input to the synchronous product is a negation of wanted behavior. Violations are found if there is a common behavior of two input automata. Scientific basis upon which formal verification is performed does not represent scientific contribution since it is something already known, but the scientific contributions are the identification of process elements relevant to the formal verification, forming a symbolic model as a transition towards the formal model, forming of the formal model, and expressing wanted/unwanted behavior. Formal verification is performed in the third phase of the proposed phased model for the development of WS-BPEL processes presented in chapter 3. Chapter 7 has introduced the implementation framework of the proposed phased model for the development of WS-BPEL processes presented in chapter 3. Tools for the implementation of proposed algorithms for visual modeling, formal verification, and static analysis are introduced as part of the implementation framework. It is concluded that any visual BPMN modeling tool providing access to the background XML code can be used for visual modeling of WS-BPEL processes since BPMN XML code is an input to the BPMN-BPEL transformation algorithm. Language-Integrated Query for C# (LINQ for C#) is used as a technology for the implementation of a bidirectional algorithm between BPMN and BPEL models, even though it is concluded that any programming language with constructs for XML document manipulation can be used for the implementation of bidirectional BPMN-BPEL transformation algorithm. eXtensible Stylesheet Language Transformations technology (XSLT) is also listed as a possible technology that can be used for the implementation of the BPMN-BPEL transformation algorithm but it is concluded that it is relatively complex when comparing it to LINQ for C# or any similar technology. The spin tool is used for the implementation of formal checking. Formal models, written in Promela syntax can be made using any textual tool. They are inputs to the formal verification performed by the Spin tool. vi Spin is the only alternative to use in the process of formal verification since it is a tool specially designed to operate with Promela syntax. Scientific contribution is the implementation of a bidirectional BPMN-BPEL transformation algorithm using LINQ for C# technology while operating with BPMN visual editors (for visual modeling) and Spin (for formal verification) is not since they are not proprietary tools. Analysis and proposals for possible tools usage also represent scientific contributions. Chapter 8 has tested the algorithms for the development of WS-BPEL processes presented in chapter 3. The BPMN-BPEL transformation algorithm was verified on an abstract WS-BPEL process as part of this chapter. Contained execution of an abstract BPMN process was transformed into corresponding WS-BPEL activities based on XML mappings defined in chapter 4. Formal verification was also verified on an abstract WS-BPEL process and it has detected all parallel variable manipulations that were present in the process. The symbolic model of the abstract WS-BPEL process was constructed according to the rules defined in chapter 6 towards the formal model upon which formal verification was performed. Scientific contributions of the dissertation with its proposed model for the phased development of WS-BPEL processes can be seen as a basis for future work to optimize it or to include other phases of development like design of services which would include: collecting user requests, identification of functionalities aggregated in services, and building services. The current model starts with the first phase of visual modeling where it is assumed that integration services already exist and their construction is not covered by any phase the model. |
