|
|
The project is organized in four research subjects:
We examine service-specific variants of criteria for reliability. We hereby focus on assuring the absence of deadlocks during the interaction of services. The problem of deadlocks is a paradigmatic problem as services interact with each other. We are sure, that the solutions of this problem can most likely be transferred to solving other problems as well.
We consider the following variants:
- Consistency. A set of services is consistent if they communicate with each other deadlock-free. For this problem we consider all involved services as input. However, this is only a realistic setting if all partners publish the control structure of their service or if the consistency can be checked with the help of the abstract view of the services involved.
- Controllability. A service is controllable if there exists another service such that the two services interact with each other deadlock-free. Controllability is a property of one service. Therefore it is possible that a provider of a service can check whether his service is controllable or not on his own. Controllability is a minimal requirement that a service must fulfill.
- Exchangeability. A service S1 is exchangeable by another service S2, if for all deadlock-free interacting sets of services containing S1, those sets of services interact deadlock-free if S1 is exchanged by S2. Exchangeability typically is regarded to two services of one partner only. Hence, this property can be checked by that partner himself.
- Abstract views. Abstract views of a service reflect some aspects of its control structure (e.g. communication activities) while abstracting from other factors. Such a view may serve as a documentation of the service within the company or it may also be used as a means to exchange information about that service with other partners. In the latter case, the degree of abstraction has to be high enough in order to hide internal company information.
- Operating guidelines. As an alternative to abstract views we analyze the automatic generation of operating guidelines. Those guidelines specify what requirements the communicating partner has to meet in order to interact with the given service deadlock-free.
We will not restrict ourselves to study those properties based on a specific language. Rather, we will use the theoretic model "open workflow-nets", which is a special class of Petri nets. This ensures a long-life cycle of our results.
For the reliability of cross-company business processes it is essential to formulate specifications adequately. Among these specifications count:
- the description of the composition structure: How are the involved services combined?
- the description of autonomy: Which degree of freedom has each of the participating partners?
- the description of transactional interrelationship: How can be assured that a process ends up in consistent states at all partners?
- the description of failure coordination: How can be reacted on faults or exceptions by a concur of all partners?
The concepts have to be developed that services can be specified company-centered, thus independently from the other partners.
We build an infrastructure to use available verification tools as well as the techniques from Subject A for processes specified in BPEL. For theses purposes we implement a compiler translating BPEL processes to Petri nets (BPEL2oWFN). These nets then can be used as the input for model checkers and other Petri net-based tools. To allow for the analysis of real-world processes the generated Petri nets have to be as small as possible.
In the project we develop technologies for a flexible model generation which allows the generation of the Petri net model from preferably abstract Petri net patterns. These patterns -- each applicable in certain contexts -- are managed in a pattern database. Static analysis of the BPEL source code helps to choose the suitable patterns.
The developed techniques are matched with the requirements of the industrial code of praxis. To this end all developments are supported by hands-on case studies. The developed tools are integrated with the MEGA business process modeling tool, used in numerous companies. This integration assures the validation of the tools in realistic scenarios. Part of the integration is an exporter and importer between BPEL and the modeling language used by the MEGA modeling tool.