The Sixth International Workshop on Automation of Software Test (AST 2011) is associated with the 33rd International Conference on Software Engineering (ICSE 2011). This edition of AST was focused on the special theme of Software Design and the Automation of Software Test and authors were encouraged to submit work in this area. The workshop covers two days with presentations of regular research papers, industrial case studies and experience reports. The workshop also aims to have extensive discussions on collaborative solutions in the form of charette sessions. This paper summarizes the organization of the workshop, the special theme, as well as the sessions.

The Service-Oriented Architecture (SOA) approach to building systems of application and middleware components promotes the use of reusable services with a core focus of service interactions, obligations, and context. Although services technically relieve the difficulties of specific technology dependency, the difficulties in building reusable components is still prominent and a challenge to service engineers. Engineering the behavior of these services means ensuring that the interactions and obligations are correct and consistent with policies set out to guide partners in building the correct sequences of interactions to support the functions of one or more services. Hence, checking the suitability of service behavior is complex, particularly when dealing with a composition of services and concurrent interactions. How can we rigorously check implementations of service compositions? What are the semantics of service compositions? How does deployment configuration affect service composition behavior safety? To facilitate service engineers designing and implementing suitable and safe service compositions, we present in this paper an approach to consider different viewpoints of service composition behavior analysis. The contribution of the paper is threefold. First, we model service orchestration, choreography behavior, and service orchestration deployment through formal semantics applied to service behavior and configuration descriptions. Second, we define types of analysis and properties of interest for checking service models of orchestrations, choreography, and deployment. Third, we describe mechanical support by providing a comprehensive integrated workbench for the verification and validation of service compositions.

Developing service compositions, using multiple standards and implementation techniques, typically involves specifying service characteristics in different languages and tools. Examples are defining service composition behaviour, in the form of the business process execution language for Web services (WS-BPEL) and a global service choreography policy, in the form of the Web service choreography description language (WS-CDL). Whilst there have been a number of model-based analysis tools reported, there is a lack of integration with development environments to support analysis of these different service artifacts. In this paper we present a short history of some of the analysis tools reported, discuss an appropriate criteria of accessible integrated development with analysis features and provide an example approach, called "service engineer" using our tools and integration work. The approach is supported by an integrated service tool-chain development environment known as the SENSORIA development environment. The aim is to provide an accessible, rigorous approach to analysing service compositions but with a simple, clearly defined interface in an integrated development environment.

This paper reports on an implementation for tool support of model-checking collaborating service compositions with deployment configurations under resource constraints.The implementation accepts UML Deployment Diagrams with an applied service deployment profile and one or more WS-BPEL orchestrations that are assigned to Web Servlets and servers in this deployment. Using model-checking techniques the tool can determine whether the configuration of deadlock-free service orchestration processes introduce deadlock scenarios when combined with resource constraints of a deployment environment. The implementation is built upon a tool suite, called WS-Engineer, which is aimed at assisting service engineers in constructing and testing various aspects of a service engineering approach, including orchestration, choreography and deployment artifacts. The tool integrates as a plug-in for Eclipse, alongside the IBM Rational software architect tool suite and others. A case study based upon a complex service grid solution, for analyzing chemical markup patterns, is used to demonstrate the accessible and practical nature of the solution.

When enacting a web service orchestration defined using the Business Process Execution Language (BPEL) we observed various safety property violations. This surprised us considerably as we had previously established that the orchestration was free of such property violations using existing BPEL model checking techniques. In this paper, we describe the origins of these violations. They result from a combination of design and deployment decisions, which include the distribution of services across hosts, the choice of synchronisation primitives in the process and the threading configuration of the servlet container that hosts the orchestrated web services. This leads us to conclude that model checking approaches that ignore resource constraints of the deployment environment are insufficient to establish safety and liveness properties of service orchestrations specifically, and distributed systems more generally. We show how model checking can take execution resource constraints into account. We evaluate the approach by applying it to the above application and are able to demonstrate that a change in allocation of services to hosts is indeed safe, a result that we are able to confirm experimentally in the deployed system. The approach is supported by a tool suite, known as WS-Engineer, providing automated process translation, architecture and model-checking views.

No abstract available.

In this paper we describe a tool for a model-based approach to verifying compositions of web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of Message Sequence Charts (MSCs), and then compiled into the Finite State Process (FSP) process algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of web service compositions can be eased through the understanding of the behavior exhibited by the composition. The approach is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling, verification and validation of the composition process.

In this paper we describe tool support for a model-based approach to verifying compositions of Web service implementations. The tool supports verification of properties created from design specifications and implementation models to confirm expected results from the viewpoints of both the designer and implementer. Scenarios are modeled in UML, in the form of message sequence charts (MSCs), and then compiled into the finite state process (FSP) algebra to concisely model the required behavior. BPEL4WS implementations are mechanically translated to FSP to allow an equivalence trace verification process to be performed. By providing early design verification and validation, the implementation, testing and deployment of Web service compositions can be eased through the understanding of the behavior exhibited by the composition. The tool is implemented as a plug-in for the Eclipse development environment providing cooperating tools for specification, formal modeling and trace animation of the composition process.

In this paper we discuss a model-based approach to verifying process interactions for coordinated Web service compositions. The approach uses finite state machine representations of Web service orchestrations and assigns semantics to the distributed process interactions. The move towards implementing Web service compositions by multiple interested parties as a form of distributed system architecture motivates the need for supporting compatibility verification of activities and transactions in all the processes. The described approach is supported by a suite of cooperating tools for specification, formal modeling and providing verification results from orchestrated Web service interactions.

In this paper, we discuss a model-based approach to verifying Web service compositions for Web service implementations. The approach supports verification against specification models and assigns semantics to the behavior of implementation model so as to confirm expected results for both the designer and implementer. Specifications of the design are modeled in UML (Unified Modeling Language), in the form of message sequence charts (MSC), and mechanically compiled into the finite state process notation (FSP) to concisely describe and reason about the concurrent programs. Implementations are mechanically translated to FSP to allow a trace equivalence verification process to be performed. By providing early design verification, the implementation, testing, and deployment of Web service compositions can be eased through the understanding of the differences, limitations and undesirable traces allowed by the composition. The approach is supported by a suite of cooperating tools for specification, formal modeling and trace animation of the composition workflow.