In the paper, we present an approach for the verification of business workflows – captured by BPEL processes – with full support for compensation and fault handling. BPEL processes are transformed into the SAL language to carry out (i) verification of safety and reachability properties and (ii) fault modeling by using the SAL symbolic model checker. Compared to existing solutions for model checking BPEL processes, the main added value of the paper is that (i) potential error propagation paths can also be assessed in addition to traditional verification tasks, and (ii) our approach scales up to relatively large workflows thanks to abstraction techniques and the use of the advanced SAL model checker.

Formal methods can effectively support the model driven develoment and analysis of IT applications in many domains. Typically, the domain-specific engineering models are transformed to formal analysis models (to compute measures that help the designer in verifying the design decisions) and verified models are mapped to test and implementation related software artefacts. An overview of four European projects demonstrates the use of support tools and tool integration facilities in development processes of systems having in sight the demand of certification according to domain-specific standards.

Electronically executed business processes are frequently implemented using the Business Process Execution Language (BPEL). These workflows may be in control of crucial business processes of an organization, in the same time existing model checking approaches are still immature i.e. they either seem to loose to much information during the generation of the analysis model, or the state space explosion prevents from model checking. We present a formal modeling technique for BPEL workflows including fault and compensation handling providing exact semantics with a state space size that allows for model checking. Additionally, error propagation among variables is supported so the effect of a faulty activity on the entire process can be examined.

We present a methodology for testing service infrastructure components described in a high-level (UML-like) language. The technique of graph transformation is used to precisely capture the dynamic aspect of the protocols which is the basis of state space generation. Then we use model checking techniques to find adequate test sequences for a given requirement. To illustrate our approach, we present the case study of a fault tolerant service broker which implements a well-known dependability pattern at the level of services. Finally, a compact Petri Net representation is derived by workflow mining techniques to generate faithful test cases in a non-deterministic, distributed environment. Note that our methodology is applicable at the architectural level rather than for testing individual service instances only.

Nowadays, due to the rapid increase in the number of available web services, more and more emphasis is put on their reliability, availability, security, etc. In order to meet such non-functional requirements, a service needs to be designed for reliability by making design decisions on a high, architectural level. Fortunately, web service related standards also include how to provide reliable messaging between services (e.g. in WS-ReliableMessaging and WS-Reliability). Several frameworks (like RAMP, RM4GS) implement the standard to provide a reliability middleware. However, these standards typically offer very low, XML-level mechanisms for specifying the reliability parameters of web services when deploying them to a reliability middleware. For this purpose, we propose a model-driven approach for the deployment of web services to standards-compliant reliable middleware. The actual XML descriptors are generated automatically from platform-independent description of services enriched with reliability attributes by model transformations.

Due to the increasing need of highly dependable services in Service-Oriented Architectures (SOA), service-level agreements include more and more frequently such non-functional aspects as security, safety, availability, reliability, etc. Whenever a service can no longer be provided with the required QoS, the service requester needs to switch dynamically to a new service having adequate service parameters after exchanging a sequence of messages. In the current paper, we first extend the core SOA metamodel with parameters required for reliable messaging in services. Then we model reconfigurations for reliable message delivery by graph transformation rules. Finally, we carry out a formal verification of the proposed rule set by combining analysis tools for graph transformation and labeled transition systems.

The integrated EU-project DECOS (Dependable Embedded Components and Systems) aims at develop-ing an integrated architecture for embedded systems to reduce life-cycle costs and to increase depend-ability of embedded applications. To facilitate the certification process of DECOS-based applications, the DECOS Test Bench constitutes a framework to support incremental Validation and Verification as well as modular certification on the basis of generic safety cases. The safety cases are based on validation-plans (v-plans) comprising the steps to validate the safety requirements (called V&V-activities). This paper focuses on two aspects of the Test Bench: the execution of V&V-activities and the integration of V&V-tools into the Test Bench framework.

The integrated EU-project DECOS (Dependable Embedded Components and Systems) aims at developing an integrated architecture for embedded systems to reduce life-cycle costs and to increase dependability of embedded applications. To facilitate the certification process of DECOS-based applications, the DECOS Test Bench constitutes a framework to support Validation and Verification. By implementing a modular approach, an application safety case merely contains the application-specific issues and reuses the safety arguments of the generic safety cases of the DECOS platform. The Test Bench covers the complete life cycle from the platform-independent models to deployment, including model validation and transformations. The safety cases are based on validation-plans (v-plans) comprising the steps to validate the safety requirements. The Test Bench provides a methods/tools repository, guidelines to generate and execute v-plans, and integration of tools and of remotely distributed test beds.

Due to the increasing need of highly dependable services in Service-Oriented Architectures(SOA), service-level agreements include more and more frequently such traditional aspects as security, safety, availability, reliability, etc. Whenever a service can no longer be provided with the required QoS, the service requester need to switch dynamically to a new service having adequate service parameters. In the current paper, we propose a metamodel to capture such parameters required for reliable messaging in services in a semi-formal way (as an extension to [1]). Furthermore, we incorporate fault-tolerant algorithms into appropriate reconfiguration mechanisms for modeling reliable message delivery by graph transformation rules.

As Web service-based system integration recently became the mainstream approach to create composite services, the dependability of such systems becomes more and more crucial. Therefore, extensions of the common service composition techniques are urgently needed in order to cover dependability aspects and a core concept for the dependability estimation of the target composite service. Since Web services-based workflows fit into the class of systems composed of multiple phases, this paper attempts to apply methodologies and tools for dependability analysis of Multiple Phased Systems (MPS) to this emerging category of dependability critical systems. The paper shows how this dependability analysis constitutes a very useful support to the service provider in choosing the most appropriate service alternatives to build up its own composite service.

We present a framework for the simulation and formal analysis of workflow models. We discuss (i) how a workflow model, implemented in the BPEL language, can be transformed into a data ow network model, (ii) how potentially incorrect execution paths can be incorporated, and (iii) how the properties of a workflow can be formally verifed using the SPIN model checker. For the several model transformation steps from workflow to analysis models, we use graph transformations.

A typical composite Web service is built of basic Web services, both internal and external, over which the integrator does not have a complete control. The service-based integration of enterprise systems raises the need for the analysis of non-functional characteristics of a composite Web service. Such an analysis should cover dependability (for instance, the reliability of the main process, sensitivity analysis on component reliability, etc.) and performability aspects (e.g. determining the optimal process structure for a given level of reliability) as well. The paper discusses how graph transformations can be used to adapt formal methodologies for analyzing SOA models. This way a flexible and extendable analysis framework can be developed for Web service-based business processes.