Conformance to functional requirements, which is also known as correctness, is a prerequisite for the quality of service of Web service compositions. This paper operationalizes correctness for Web service compositions. It also proposes a requirements framework for service-oriented modeling techniques so that correctness can be shown by verification and Web service compositions can be modeled intuitively.

1 Motivation and object of research

Web services and Web service compositions (WS compositions) are currently considered to be the most widespread possibility for implementing service-oriented architectures (Erl 2004; Newcomer and Lomow 2005). A (basic) Web service is a software system that exposes its functionality by means of a machine-processable interface consisting of several operations. It enables (asynchronous) message-based machine-to-machine interaction over a network (Booth et al. 2004). Web services are offered by internal IT departments or by external service providers. A WS composition is a Web service that realizes complex functionality by coordinating multiple (component) Web services in transactions (Alonso et al. 2004, p. 141). Analogous to (basic) Web services, WS compositions expose their functionality via interfaces. In this paper, WS compositions refer to the orchestration of Web services, not to their choreography (Dostal et al. 2005, p. 226).

According to a survey of the Yankee Group, WS compositions raise high expectations (Kallus 2004). Among other things, they are expected to improve business processes and to foster the integration of existing e-business, CRM, SCM, and ERP initiatives. Already in 2004, more than 50 % of the US companies relied on Web services whereof 60 % estimated their impact on business-to-business integration (very) high. However, designing and running WS compositions is error-prone. Involved teams of software engineers and modelers usually come from multiple companies and have different skills, experiences, or functional backgrounds. Web services are usually managed by different companies and may not have been developed for composition. Analogous to other distributed systems based on asynchronous communication, it is difficult to anticipate how WS compositions behave during execution and whether they conform to the functional requirements identified during requirements engineering. Errors, however, may violate service level agreements. This may cause losses or penalties and have negative impact on the reputation of the companies involved. Therefore, it is an important task to make sure that WS compositions conform to their functional requirements.

A possibility of reliably showing conformance to functional requirements is verification. In this context, conformance to functional requirements is also called correctness. The idea of verification dates back to Floyd (1967) and Hoare (1969). In contrast to testing, for instance, where correctness can only be shown with respect to selected test data, verification aims at exhaustively proving correctness for all behavioral facets and inputs of a given program. During verification, the program is analyzed automatically. This requires the semantics of each program statement to be defined unambiguously. A program is said to be correct if its implementation (i. e. its program code or a corresponding formal model) is consistent with a corresponding specification of behavioral claims (i. e. functional requirements on the program’s behavior) (Balzert 1998, pp. 445–472).

Despite the need for correctness, research focuses on non-functional requirements such as availability, scalability, capacity, etc. (Lee et al. 2003), which are already known from network research. Current approaches to (Web) service-oriented modeling do not (or hardly) cope with correctness and verification. This includes specification languages like the de facto standard WS-BPEL (Alves et al. 2007) – despite some attempts (e. g. Farahbod et al. 2005; Stahl 2005; Moser et al. 2007; Lohmann 2007) – and high-level approaches (Arjansani 2004; Bell 2008; Papazoglou and van den Heuvel 2006; Zimmermann et al. 2004). Current approaches to the verification of Web services (WS verification) require formal models, e. g. in terms of finite state automata or Petri nets, which are not necessarily intuitive for conceptual modelers. Such approaches also postulate a variety of formal claims on WS compositions so that it is not clear what correctness actually means.

Against this background, we address the following research questions: How does correctness have to be operationalized so that it fits the peculiarities of WS compositions? How do (Web) service-oriented modeling techniques have to be shaped so that correctness can be shown by verification and WS compositions can be modeled intuitively?

This paper relies on a design-oriented, deductive, and argumentative research approach (Hevner et al. 2004; Wilde and Hess 2007). In section 2, we identify the research gap by compiling current approaches to WS verification and service-oriented modeling. Section 3 proposes a definition of correctness and a requirements framework as artifacts. Section 4 aims at showing the framework’s basic applicability in the sense of a basic evaluation. Section 5 briefly summarizes the findings and points out further research.

2 State of the art

As for WS verification, the most frequently applied verification method is model checking (Clarke et al. 2001; Schneider 2004). This is because model checking is particularly suitable for verifying distributed systems of multiple components that interact via message exchange. WS compositions are such distributed systems. In contrast to other verification methods, model checking does not directly work on implementations in the sense of program code, but on formal models that focus on relevant details such as exchanged messages and their content. A variety of model checking-based approaches has been proposed for WS verification (van Breugel and Koshkina 2006). WS compositions are usually modeled by means of finite state automata (e. g. Fu et al. 2004a), Petri nets (e. g. Martens 2005; Rozinat and van der Aalst 2008; Schlingloff et al. 2005), abstract state machines (e. g. Fahland and Reisig 2005; Farahbod et al. 2004), or process algebras (e. g. Ferrara 2004). Some approaches are also capable of translating XML-based models of WS compositions (see below). Behavioral claims are commonly formalized by means of temporal logics. This is because it enables to reason about the content and temporal interdependencies of exchanged messages without introducing time explicitly (Clarke et al. 2001, p. 4).

In the following, we do not discuss the approaches in their entirety, but focus on how they deal with correctness and behavioral claims. Most approaches enable to specify behavioral claims that refer to concrete use cases. This aim is achieved by employing temporal logics as just mentioned. Some approaches additionally postulate claims that do not refer to concrete use cases. This is mostly done with respect to the formalism employed. The following list shows selected claims of the latter category:

 

  • Usability requires a WS composition to terminate properly (Martens 2005, p. 26; Schlingloff et al. 2005, p. 11; Kopp et al. 2006).

  • Syntactic compatibility requires that two Web services can be composed with respect to their interfaces, i. e. names of messages (Martens 2005, p. 23).

  • Semantic compatibility requires that the composition of two Web services fulfills the usability claim (Martens 2005, p. 26).

  • Fitness indicates up to which percentage the behavior of a WS composition conforms to its implementation (Rozinat and van der Aalst 2008, p. 67).

  • Appropriateness indicates whether the implementation of a WS composition adequately characterizes the observed behavior (Rozinat and van der Aalst 2008, p. 67).

 

Beyond, there are also claims on the equivalence of WS compositions (Martens 2005, p. 27; Kopp et al. 2006) or on whether the communication pattern of multiple Web services could be simulated by synchronous message exchange (Fu et al. 2004a, p. 627). As these claims refer to correctness at best indirectly, they are omitted for the further discussion.

The following is noteworthy: No approach states how the claims it proposes refer to the overall concept of correctness. It remains unclear whether any subset of these claims would be sufficient, whether (or how) claims of several approaches cohere, and whether they fit the peculiarities of WS compositions. Some claims depend on the underlying formalism (e. g. usability was defined for Petri nets), others are too generic (e. g. syntactic compatibility refers to the names of messages, semantic compatibility is limited to termination). It is not discussed whether these claims can be structured. In conclusion, there is a research gap with respect to how correctness can be operationalized so that it fits the peculiarities of WS compositions.

When presenting an operationalization in the next section, we adopt several existing ideas in order to provide an incremental contribution. We adopt the idea that there are claims that refer to concrete use cases and others that do not. The latter category, for instance, would include usability as termination-related requirement. We extend syntactic compatibility from message names to operations and parameters. This is appropriate because correctness rather depends on the content of exchanged messages. We also extend semantic compatibility to possible (input and output) values and value ranges of parameters (see below) as well as to behavioral claims referring to concrete use cases. This enables to reason about sequences of exchanged messages and concrete behavior. We omit fitness as we consider correctness as a dichotomous property, that is, a WS composition is either correct or not. We also omit appropriateness as is takes on a contrary perspective by indicating whether an implementation characterizes observed behavior well. As additional contribution, we structure correctness by means of a system-theoretic perspective. This is suitable as each WS composition can be characterized by structure and behavior. In general, claims on a WS composition’s structure (e. g. syntactic compatibility) do not require verification as they deal with static aspects. Behavioral claims, in contrast, require verification as they address dynamic aspects. This distinction enables to assess correctness in a less complex manner.

As for (Web) service-oriented modeling, there are technical XML-based specification languages and comprehensive high-level approaches. With respect to the former category, service interfaces, operations, and parameters are formalized by means of the Web Service Description Language (WSDL) (Christensen et al. 2001). Messages exchanged to invoke other services’ operations are commonly specified in terms of SOAP (Mitra 2003). WS compositions are specified by means of the Web Services Business Process Execution Language (WS-BPEL) (Alves et al. 2007), the Web Services Choreography Description Language (WSCDL) (Kavantzas et al. 2005), the Business Process Modeling Language (BPML) (Dubray 2008), or the Web Service Choreography Interface (WSCI) (Arkin et al. 2002) (for an overview see e. g. Peltz 2003). In the context of the Semantic Web, there are specification languages for modeling the semantics of operations and parameters, e. g. possible (input and output) values and value ranges. They include the Resource Description Framework (RDF) (Klyne and Carroll 2004) and the Web Ontology Language for Web services (OWL-S) (Martin et al. 2004) (for an introduction see e. g. Herman 2003). As for high-level approaches, three examples are presented here. The service-oriented modeling and architecture approach proposes a framework for service identification, specification, and realization including role models for service providers and consumers (Arjansani 2004; Zimmermann et al. 2004). The service-oriented modeling framework is a high-level map depicting the various components that contribute to a service-oriented modeling approach, namely conceptual, analysis, and logical environment (Bell 2008, p. 23). The service-oriented design and development methodology covers the entire service development lifecycle from service analysis and design to service execution and monitoring (Papazoglou and van den Heuvel 2006). It illustrates each phase in detail and proposes general design principles for SOA. It also acknowledges the importance of correctness (Papazoglou and van den Heuvel 2006, p. 435).

The high-level approaches do not elaborate on how service-oriented modeling techniques should be shaped so that correctness can be shown by verification while WS compositions can be modeled intuitively. Moreover, the specification languages from above, e. g. WS-BPEL, are currently not or hardly amenable to verification. Thus, there also is a research gap. As the high-level approaches do not provide any concrete hint on how to integrate verification, it is not possible to make an incremental contribution. Therefore, we examined general requirements of verification and conceptual modeling with respect to WS compositions and tried to integrate them into a requirements framework. Moreover, we used the specification languages in order to define the structural requirements of correctness independent of the formalisms for WS verification.

In the following, we operationalize correctness based on the deliberations from above. We then elaborate on the requirements framework.

3 Artifacts

3.1 A definition of correctness for web service compositions

We analyze correctness from a system-theoretic perspective. This seems appropriate because WS compositions can be interpreted as general systems characterized by structure and behavior (Ferstl and Sinz 2006, p. 12). The structure of a WS composition encompasses the WS composition itself, the component Web services, and the message types they may exchange. The latter are given by the WS composition’s invocation statements and by the operations of the component Web services’ interfaces. The behavior of a WS composition represents the actual interaction among the WS composition and its component Web services. This includes the set of all message sequences (i. e. sequences of operation invocations). In accordance with this point of view, we propose that correctness splits into structural and behavioral correctness.

3.1.1 Structural correctness

WS compositions virtually have two interfaces: a “provides interface” and a “requires interface” (Sommerville 2004, p. 444). The former comprises the operations by which a WS composition provides its functionality to other Web services. The latter includes the operations a WS composition requires in order to implement its functionality. Component Web services only have a “provides interface” because they are only known from an external perspective.

Structural correctness requires that for each operation of the WS composition’s “requires” interface there is at least one identically named operation in a component Web service’s “provides” interface that matches with respect to number, sequence, and types of parameters. One possibility to check this is to compare the component Web services’ WSDL interfaces and the invocation statements of the WS composition’s WS-BPEL specification. If mandatory and optional parameters are distinguished, only mandatory parameters need to match. If the WS composition and the component Web services are semantically annotated, operations also have to match with respect to possible (input and output) parameter values or value ranges, for instance. It is not necessary that each operation of the component Web services’ “provides” interfaces has a matching operation in the WS composition’s “requires” interface. This is because component Web services may of course provide more functionality than required.

In many cases, component Web services are discovered and selected at run time. WS compositions may be executed although not all required operations are available. In contrast, state-of-the-art verification techniques (e. g. Fu et al. 2004a; Martens 2005) require all operations to be available and models of WS compositions to be completely specified. Otherwise, they cannot be processed by verification tools and correctness cannot be analyzed. That is, if a component Web service is not available, one can neither reason about its own behavior nor its implications on the WS composition’s global behavior. To overcome this discrepancy, verification could take place at design time or be shifted to the point in time during execution where all component services have been selected. As WS compositions and/or behavioral claims may have to be changed after verification, one would have to accept human interaction in the latter case.

3.1.2 Behavioral correctness

Behavioral correctness requires sequences of messages to conform to a set of behavioral claims. As messages can only be exchanged if required and provided operations match and all required operations are provided, structural correctness is a prerequisite of behavioral correctness. In literature, behavioral claims split into safety claims and liveness claims (Schneider 2004, p. 14). Safety claims are claims that must not be violated, whereas liveness claims must always hold (Holzmann 2003, p. 74). This distinction does not sufficiently characterize behavioral correctness of WS compositions. What is missing is a complementary distinction between application-independent and application-dependent claims (see section 2). This allows to separate generic claims for many use cases from particular claims for only a couple of use cases, which fosters reusability.

 

  • Application-independent claims: Claims that cover generic issues resulting from the distributed and asynchronous nature of WS compositions are called application-independent claims. They occur in many use cases and may be captured in a rather standardized manner. There are application-independent safety and liveness claims. Typical claims of the former category are mutual exclusion and deadlock freedom. Mutual exclusion guarantees the integrity of business data (e. g. available stock, account balances) by ensuring that shared variables or other critical sections are never accessed by more than one component Web services at the same time. Deadlock freedom is necessary for the termination of WS compositions. Otherwise, it would be possible that two or more component Web services wait for one another. A typical claim of the latter category is starvation freedom, which is closely related to termination and deadlock freedom. A Web service is said to starve if it has requested a resource (e. g. a document or a database entry) that is currently being held by another Web service not willing to release it. Starvation freedom guarantees by means of some fairness policy that each request for a resource is eventually satisfied.

  • Application-dependent claims: Claims that vary with a WS composition’s use case are called application-dependent claims. They are much more difficult to discover because they are only valid for some or only one use case. For this reason, it is impossible to enumerate them exhaustively. Some claims occur more than once and can be structured into catalogs of domain-specific claims. For example, there might be a catalog for commercial applications. A corresponding safety claim may be that customers do not have to pay for goods they have not ordered. A corresponding liveness claim may be that each customer who places an order will eventually receive an invoice. The advantage of this catalog is that it applies to all use cases where customers order goods or services. Nevertheless, some application-specific claims apply to just one scenario so that they need to be assessed individually.

 

Tab. 1 summarizes the types and examples of behavioral claims.

Tab. 1 Types and examples of behavioral claims
Full size table

3.2 A requirements framework for service-oriented modeling techniques

Now that correctness has been examined, it is assessed what requirements (Web) service-oriented modeling techniques have to meet so that correctness can be shown by verification and WS compositions can be modeled intuitively. Therefore, we propose a requirements framework considering two complementary perspectives: formal foundations and modeling support.

 

  • Formal foundations: Verification requires models and specifications of WS compositions to conform to formal languages and their semantics to be defined unambiguously (Balzert 1998, p. 467). This enables to “compute” all behavioral facets of WS compositions and to check which of them violate the specification. Only formally well-founded models and specifications are amenable to verification tools.

  • Modeling support: Whereas requirements on formal foundations are compulsory with respect to technical amenability to verification, modeling techniques should also consider the modelers’ capabilities and limitations of information processing. This is important for several reasons: First, in the context of business and information systems engineering as an inter-discipline, models aim at reducing complexity and at fostering the communication among modelers and model users (Ferstl and Sinz 2006, p. 123). Second, in the context of WS compositions, modelers from different enterprises with different skills, experiences, and functional backgrounds cooperate. Third, verification tools operate on a technical level so that their output is difficult to understand for conceptual modelers. Fourth, modeling behavioral claims is error-prone so that modeling tools should support modelers as good as possible.

 

Tab. 2 shows the requirements framework. In the following, each requirement will be presented. The formalization of models of WS compositions requires formal syntax and formal semantics.

 

  • Formal syntax: The syntax of a modeling language encompasses elements as well as rules that prescribe how to combine elements. To cover the behavioral facets of WS compositions, elements for manipulating the conversational state (e. g. assignment of variables), message exchange (e. g. synchronous and asynchronous send / receive), and control flow (e. g. conditions, iterations, concurrency) are necessary. Syntax is formal if it is specified in terms of non-prosaic meta models or mathematic models.

  • Formal semantics: Semantics builds upon syntax and deals with the meaning of elements. The semantics of a WS composition represents its behavior resulting from the interplay of its elements. It should deal with issues of distributed and asynchronous systems such as concurrency and non-determinism. Most modeling languages in the field of business and information systems engineering provide formal syntax, only few provide formal semantics.

 

The formalization of specifications requires a formal language for behavioral claims, e. g. temporal logics as mentioned above. With models and specifications serving as input for the same verification tool, it is important that this formalism complies with the modeling language employed for describing the semantics.

Tab. 2 Requirements framework for service-oriented modeling techniques
Full size table

 

Modeling support requires a process model that guides the modeler through the process of modeling and verifying WS compositions. In particular, the process model should include the modeling of specifications and their harmonization with models of WS compositions. It should contain a “loop” from verification back to the modeling of models and specifications because models and specifications may need to be modified several times after verification.

Beyond, modeling techniques are requested to provide modeling and verification tools that fulfill the following requirements:

 

  • Reduction of complexity: As models of WS compositions typically refer to multiple business partners and represent complex behavior, they easily overstrain the modelers’ capacity of information processing. Modeling tools should provide graphical means for reducing complexity. Especially the interfaces of WS compositions enable modelers to switch between internal and external perspectives and to focus on a particular section of a model.

  • Visualization of behavior: Behavior is often visualized in a static manner. That is, carriers of behavior (e. g. activities, functions, tasks) are identified and related according to their temporal or behavioral logic. This does not correspond to human imagination. Modeling tools should be able to simulate the execution of WS compositions. Modelers should be able to chose among different execution possibilities and get an intuitive awareness of possible errors and bottlenecks.

  • Integrated modeling of WS compositions and specifications: Models and specifications of WS compositions cohere closely as they represent actual and expected behavior respectively. Additionally, the formalization of behavioral claims is error-prone and needs to be harmonized with the peculiarities of concrete representations of WS compositions. Modeling tools should enable the integrated modeling of WS compositions and specifications.

  • Constructive feedback: If behavioral claims are violated, the reasons may not be immediately obvious. This is for two reasons: First, models and/or specifications may contain errors. Second, errors are difficult to reconstruct in a distributed environment. Verification tools should provide modelers with constructive feedback on where and under what circumstances behavioral claims are violated. As this feedback typically is highly technical, modeling tools should furthermore be able to represent this feedback in a way understandable for modelers.

 

We hypothesize that modeling techniques that meet these requirements enable to show correctness by verification and to model WS compositions intuitively.

4 Basic evaluation of the requirements framework

In order to provide a basic evaluation, we will now analyze whether the requirements framework is principally applicable. In the following, we present a selected approach, analyze it with respect to the requirements, and assess whether this leads to reasonable findings. The approach is that of Fu et al. (2004a; Fu et al. 2004b; Fu et al. 2005; Fu et al. 2006). It has been chosen because it is an elaborate framework for analyzing, designing, and verifying WS compositions (Fu et al. 2004a, p. 622), has already been applied to WS-BPEL processes, relies on the state-of-the-art model checker SPIN (Holzmann 2003), and has been published in several international journals and conferences. In order to be more illustrative, we refer to a widely known example from the previous WS-BPEL version known as BPEL4WS version 1.1 (Andrews et al. 2003).

The example is as follows: A bank intends to acquire more business customers (BIZ). A survey disclosed that business customers complain about administrative overhead when applying for short-term loans of moderate value. The board has decided to improve the process: Future loan applications will be classified by amount and risk. The latter will be assessed by an external association of experts (ASS). Only critical applications, i. e. those with an amount higher than or equal to 10,000 Euros or with high risk, will be examined by in-house loan approvers (APP). Business customers should apply via the Internet. As both the external experts and the internal loan approvers offer their functionality by means of Web services, the additional functionality will be implemented by means of a WS composition. Thereby, the bank unites its loan approval authority and external risk assessment competences in a single loan service composition (LNS). The bank is interested in that the loan service composition conforms to the following two application-dependent functional requirements (behavioral claims): First, loan applications with a high amount must be investigated in detail because, according to Basel II, each loan has to be guaranteed with a risk-dependent amount of equity. Second, in order to satisfy its customers’ needs, each loan application of less than 10,000 Euros and low risk should be granted.

Technically speaking, the WS composition (LNS) coordinates the functionality of two Web services (APP and ASS), and is used by a third Web service (BIZ). Three message types are necessary: request messages (req) that contain the requested amount of money (amount), approval messages (app) that contain the bank’s decision (result), and risk assessment messages (ass) that contain the risk classification (risk).

In the approach of Fu et al., WS compositions are modeled by means of guarded finite state automata (GFSA). Informally speaking, finite state automata consist of states and transitions. States store information about the past. Transitions convey automata from one state to another upon external stimuli, e. g. sent or received messages. In order to deal with the content of messages, send-transitions are annotated with guards. Analogous to production rules, each guard consists of a condition part and an action part. The former specifies the transition’s precondition. The latter specifies the content of the message being sent. Guards are formalized by means of XPath (Clark and DeRose 1999). Receive-transitions are not guarded because the content of received messages cannot be controlled.

Fig. 1 shows how the example can be modeled by means of GFSA. We use the standard notation for automata. States are modeled as circles, transitions as directed edges. Final states are modeled as two concentric circles, initial states as circles with edges that point to them from “nowhere”. Each transition has two annotations. The first annotation indicates which message is currently being sent (!) to or received (?) from which automaton. We use indexes to distinguish several message instances of the same type (e. g. req1, req3). The second annotation (in squared brackets) specifies the guard. We use apostrophes to characterize that messages are forwarded (req3’ = req1) or new values are assigned to variables (e. g. app1‘.risk = “low”). For each WS composition and Web service, there is an automaton. Let us, for instance, consider the loan assessor’s automaton (ASS). In its initial state, the automaton is waiting for a request message (req3) forwarded by the loan service composition (?req3←LNS). After that, the assessors’ risk classification is returned to the loan service composition (LNS) via a risk assessment message (ass1) (!ass1→LNS). As the result can be “high” or “low”, the corresponding transition indicates both possibilities. As ass1 can always be sent, the guard condition is true.

Fig. 1
figure 1

The example scenario modeled with guarded finite state automata (GFSA)

Full size image

Behavioral claims are formalized by means of Linear Time Temporal Logic (LTL), which counts among temporal logics (see section 2). LTL extends propositional logic by temporal operators. These indicate how propositional expressions (e. g. specific variable assignments) cohere in time (Holzmann 2003, p. 135). Two exemplary temporal operators – which will be useful below – are globally (G) and eventually (F). The former requires that the propositional expression to which it refers remains true throughout the run of the automata (i. e. the execution of the WS composition). The latter requires that the propositional expression to which it refers becomes true at least once during the run of the automata. As each LTL formula can be transformed into a GFSA (Vardi and Wolper 1986, p. 332), it is useful to use both approaches together.

Let us, for instance, formalize the second behavioral claim from above. It requires req 1 to contain an amount of less than 10,000 Euros (req 1.amount < 10,000), ass 1 to indicate “low” risk (ass 1.risk = ”low”), and app 2 to indicate acceptance (app 2.result = ”yes”). Temporally speaking, the claim must hold throughout the entire execution. Thus, it must be globally (G) true. The fact that req 1 and ass 1 lead to app 2 is modeled as implication (→). Although it is not known when exactly app 2 is returned, it must eventually (F) be returned. Together, these considerations result in the following LTL formula: G(req 1 .amount <10,000 ∧ ass 1 .risk = “low” → F(app 2 .result = “yes”)). This formula can be translated into an automaton and serve – together with the automata from above – as input for the model checking tool SPIN, which analyzes whether the claims holds or not.

How does the approach of Fu et al. conform to the requirements framework from above? With respect to formal foundations, GFSA provide formal syntax and semantics that cover the behavioral facets of WS compositions. LTL enables to formalize both application-independent and application-independent behavioral claims. It also complies with GFSA. As for modeling support, the approach provides a verification-centered process model that is implemented by the proprietary tool WSAT (Web Service Analysis Tool) (Fu et al. 2004b). This tool, however, does not enable to model WS compositions and specifications, neither separately nor jointly. Both must be modeled by hand. Modelers have to cope with the complexity on their own. The employed model checking tool SPIN provides constructive feedback. This feedback, however, is presented in a technical way and only hardly suitable for conceptual modelers. Summing up, according to the requirements framework, the approach could be improved in the following ways: First, the tool should enable to model behavioral claims together with WS compositions (ideally in a graphical manner). Second, this tool should be integrated with the verification tool so that the feedback of the verification process can be integrated with the representation of WS compositions.

It may be stated that the analysis leads to reasonable results. Each requirement could be assessed. It could be pointed out how the approach of Fu et al. can be improved. This corroborates our hypothesis from above – at least basically and in the sense of principle applicability.

5 Summary and further research

We addressed the research gap with respect to how correctness can be operationalized for WS compositions and how (Web) service-oriented modeling techniques should be shaped so that correctness can be shown by verification and WS compositions can be modeled intuitively. We propose to split correctness into structural and behavioral correctness. The former requires the interfaces of WS compositions and component Web services to match with respect to operations and parameters. The latter requires the behavior of WS compositions to conform to specifications of application-independent and application-dependent behavioral claims. The proposed requirements framework covers the perspectives “formal foundations” and “modeling support”. The first perspective requires formal syntax and semantics for models of WS compositions and a compatible formalism for behavioral claims. The second perspective requires a process model as well as modeling tools that reduce modeling complexity, visualize the behavior of WS compositions, integrate models of compositions and specifications, and integrate the feedback of verification tools. The requirements framework has been basically evaluated by analyzing an example approach.

The results will be subject to the following research:

 

  • The framework comprises requirements on a conceptual level. We have only assessed for one example approach how it could be improved, i. e. refined or extended, in order to meet the requirements. This is where further research in the sense of a comprehensive survey would be useful.

  • The requirements framework focuses on formal foundations and modeling support. It does not provide an economic perspective on verification. Showing correctness leads to overheads. This is because specifications have to be created, models have to be verified, and specifications and/or models may have to be modified repeatedly. However, for many use cases it cannot be stated in advance whether the utility realized by preventing erroneous WS compositions justifies this overhead. This economic trade-off constitutes an interesting field for further research.