Law

Generating Interface Grammars from WSDL for Automated Verification of Web Services

Categories
Published
of 15
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Related Documents
Share
Description
Generating Interface Grammars from WSDL for Automated Verification of Web Services Sylvain Hallé, Graham Hughes, Tevfik Bultan, and Muath Alkhalaf University of California Santa Barbara, CA
Transcript
Generating Interface Grammars from WSDL for Automated Verification of Web Services Sylvain Hallé, Graham Hughes, Tevfik Bultan, and Muath Alkhalaf University of California Santa Barbara, CA USA Abstract. Interface grammars are a formalism for expressing constraints on sequences of messages exchanged between two components. In this paper, we extend interface grammars with an automated translation of XML Schema definitions present in WSDL documents into interface grammar rules. Given an interface grammar, we can then automatically generate either 1) a parser, to check that a sequence of messages generated by a web service client is correct with respect to the interface specification, or 2) a sentence generator producing compliant message sequences, to check that the web service responds to them according to the interface specification. By doing so, we can validate and generate both messages and sequences of messages in a uniform manner; moreover, we can express constraints where message structure and control flow cannot be handled separately. 1 Introduction Service-oriented architecture (SOA) has become an important concept in software development with the advent of web services. Because of their flexible nature, web services can be dynamically discovered and orchestrated to form value-added e-business applications. However, this appealing modularity is the source of one major issue: while dynamically combining cross-business services, how can one ensure the interaction between each of them proceeds as was intended by their respective providers? Achieving modularity and interoperability requires that the web services have well defined and enforceable interface contracts [20]. Part of this contract is summarized in the service s WSDL document, which specifies its acceptable message structures and request-response patterns. This document acts as a specification that can be used both to validate and to generate messages sent by the client or the service. This double nature of WSDL makes it possible to automatically produce test requests validating the functionality of a service, or to test a client by communicating with a local web service stub that generates WSDL-compliant stock responses. As it is now well known, many web services, and in particular e-commerce APIs such as the Amazon E-Commerce Service, Google Shopping or PayPal, This work is supported by NSF grants CCF and CCF WSDL Specification WSDL to Interface Grammar Translator Interface Grammar Control Flow Constraints Interface Compiler Web Service Client SOAP Request SOAP Response Server Stub Service Driver SOAP Request SOAP Response Web Service Server Fig. 1: Our web service verification framework introduce the notion of sessions and constrain communications over several request-response blocks. The previous approach does not generalize to such scenarios. Apart from attempts at validation of service interactions through runtime monitoring of message sequences [5,6,13,14,18], for the most part the question of generating a control-flow compliant sequence of messages, for simulation, testing or verification purposes, remains open. Interface grammars are a specification formalism that has been proposed to enable modular verification [16]. An interface grammar specifies the allowable interactions between two components by identifying the acceptable call/return sequences between them. In earlier work, we proposed their use for expressing the control-flow constraints on a client interacting with a web service [17]. However, message elements in these grammars were regarded as terminal symbols; to actually generate or validate a given message, hand-coded Java functions had to be written and hooked to their respective grammar counterpart. In this paper, we bridge the gap between control flow and message specifications by developing an automated translation of WSDL documents into interface grammar rules. In Section 2, we present a real-world web service, the PayPal Express Checkout API. We exhibit constraints where the sequence of allowed operations and their data content are correlated, and express them with the use of interface grammars. Our web service verification framework (Figure 1) consists of two tools: 1) a WSDL-to-interface grammar translator and 2) an interface compiler. First, the WSDL to interface grammar translator takes a WSDL specification as input and converts it into an interface grammar; this translation is described in Section 3. Constraints that are not expressed in WSDL (such as control-flow constraints) can then be added to this automatically generated interface grammar. In Section 4, we use an interface compiler which, given an interface grammar for a component, automatically generates a stub for that component. This stub acts a parser for incoming call sequences; it checks that the calls conform to the grammar and generates return values according to that grammar. Moreover, the same grammar can be used to create a driver that generates call sequences and checks that the values returned by the component conform to it. The compiler 2 was applied to perform both client and server side verification on two real-world services, including PayPal s Express Checkout, and allowed us to discover a number of mismatches between the implementation of the services and their documentation. In addition to being feasible and efficient, our approach differs from related work mentioned in Section 5 by enabling us to validate and test properties where control flow and message content cannot be handled separately. 2 Web Service Interface Contracts An interface contract is a set of conventions and constraints that must be fulfilled to ensure a successful interaction with a given web service. Elicitation and enforcement of such contracts has long been advocated [20], and interface documents such as WSDL provide a basic form of specification for syntactical requirements on SOAP messages and request-response patterns. Although many web services are composed of such simple request-response patterns of independent operations, in practice a fair number of services also exhibit long-running behavior that spans multiple requests and responses. This is especially true of commerce-related web services, where concepts such as purchase transactions and shopping carts naturally entail some form of multi-step operations. 2.1 The PayPal Express Checkout API A commercial web service suite provided by the PayPal company, called the PayPal Web Service API, is an example of a service that supports multi-step operations. Through its web site, PayPal allows to transfer money to and from credit card and bank accounts between its registered members or other financial institutions. In addition to direct usage by individuals, an organization wishing to use these functionalities from its own web site can do so through PayPal s web service API. All transactions can be processed in the background between the organization and PayPal by exchanging SOAP messages that replace the standard access to PayPal s portal. PayPal s API is public and its documentation can be freely accessed [1]. The sum of all constraints, warnings, side notes and message schemas found in this documentation constitutes the actual interface contract to the web service API. We shall see that this contract is subject to data and control-flow constraints, and that these constraints can be formally specified using interface grammars. To illustrate our point, we concentrate on a subset of PayPal s API called Express Checkout, which allows for a simplified billing and payment between an organization and a customer. The organization simply sends PayPal a total amount to be charged to the customer; PayPal then performs the necessary background checks and confirmations with the customer, after which the organization retrieves a transaction number which can be used to execute the money transfer. Express Checkout is performed in three steps, each corresponding to a requestresponse pattern of XML messages. The first step is to create an Express Checkout instance through the SetExpressCheckout message, whose structure, defined 3 PaymentDetails Token 1234 /Token OrderTotal 50 /OrderTotal PaymentDetailsItems PaymentDetailsItem Name ... /Name Number ... /Number Quantity ... /Quantity Amount ... /Amount /PaymentDetailsItem ... /PaymentDetailsItems PaymentAction Sale /PaymentAction /PaymentDetails Token ... /Token PayerID ... /PayerID PaymentDetailsItems ... /PaymentDetailsItems (b) GetExpressCheckoutDetails (a) SetExpressCheckoutRequest Token ... /Token PayerID ... /PayerID PaymentDetailsItems ... /PaymentDetailsItems PaymentAction Sale /PaymentAction (c) DoExpressCheckoutPaymentRequest Token ... /Token PaymentInfo TransactionID ... TransactionID GrossAmount ... GrossAmount PendingReason ... PendingReason /PaymentInfo (d) DoExpressCheckoutPaymentResponse Fig. 2: Request and response messages from PayPal s Express Checkout API in the WSDL specification, is shown in Figure 2a. This message provides a total for the order, as well as (optionally) a list of items intended to detail the contents of the order the client is billed for. PayPal s response to this message consists of a single Token element, whose value will be used in subsequent messages to refer to this particular instance of Express Checkout. The PaymentAction element (Figure 2c) can take the value Sale, indicating that this is a final sale, or Authorization and Order values indicating that this payment is either a basic or an order authorization, respectively. The second step consists of obtaining additional details on the Express Checkout through the GetExpressCheckoutDetails operation. The request message simply requires a token identifying an Express Checkout instance; the response to this message is structured as in Figure 2b. It repeats the payment details and token fields from the previous request, and adds a PayerID element. This element is then used in the last operation, DoExpressCheckoutPayment (Figure 2c); the response to this message (Figure 2d) completes the Express Checkout procedure. 2.2 Interface Grammars for Web Services Interface grammars were proposed as a new language for the specification of component interfaces [15,16]. The core of an interface grammar is a set of production rules that specifies all acceptable method call sequences for the given component. An interface grammar is expressed as a series of productions of the form a(v 1,..., v n ) A. The v 1,..., v n are lexically scoped variable names corresponding to the parameters of the non-terminal a. A is the right hand side of the production, which may contain the following: 4 start!seco(doc 1, items, token, action); seco(doc 2, token); start; details(items, token, action, payerid); start ǫ details(items, token, action, payerid)!gecod(doc 1, token); gecod(doc 2, token, payerid); do(items, token, action, payerid) do(items, token, Sale, payerid)!decop(doc 1, token, payerid, items, Sale ); decop(doc 2, token, transactionid) do(items, token, action 1, payerid)!decop(doc 1, token, payerid, items, action 2); decop(doc 2, token, transactionid) Fig. 3: Interface grammar for a PayPal Express Checkout client nonterminals, written nt(v 1,..., v n ); semantic predicates that must evaluate to true when the production is used during derivation, written p ; semantic actions that are executed during the derivation, which we express as a ; incoming method calls, written?m(v 1,..., v n ); returns from incoming method calls, written m(v 1,..., v n ); outgoing method calls, written!m(v 1,..., v n ); returns from outgoing method calls, written m(v 1,..., v n ). For the purposes of web service verification, the method calls in the interface grammar correspond to the web service operations. For example, the interface grammar shown in Figure 3 represents the client interface for a simplified version of the PayPal service described previously. Terminal symbols seco, gecod and decop stand respectively for operations SetExpressCheckout, GetExpress- CheckoutDetails and DoExpressCheckoutPayment; the! and symbols denote the request and response message for each of these operations. The? and symbols, which are not used in our example, would indicate that the server, instead of the client, initiates a request-response pattern. Nonterminal symbols in interface grammars are allowed to have parameters [15]. The doc i symbol in each message refers to the actual XML document corresponding to that particular request or response; it is assumed fresh in all of its occurrences. Remaining parameters enable us to propagate the data values from that document that might be used as arguments of the web service operations. Because we need to be able to pass data to the production rules as well as retrieve them, we use call-by-value-return semantics for parameters. By perusing PayPal s API documentation, it is possible to manually define the simple interface grammar shown in Figure 3, which captures a number of important requirements on the use of the PayPal API: 1. Multiple Set, Get and Do operations for different tokens can be interleaved, but, for each token, the Set, Get and Do operations must be performed in order. 5 2. The PayerID field in the DoExpressCheckoutPaymentRequest must be the one returned by the GetExpressCheckoutDetails response with matching Token element. 3. If the action element of the SetExpressCheckout operation is set to Sale, it cannot be changed in the DoExpressCheckoutPayment; otherwise, the Get and Do operations can have different action values. 4. To ensure that every Express Checkout instance is eventually complete, every SetExpressCheckout operation must be matched to subsequent GetExpress- CheckoutDetails and DoExpressCheckoutPayment requests. Although all these constraints are mentioned in the service s documentation in some form or another, none of them can be formally described through the WSDL interface document. 3 Translating WSDL to Interface Grammars While interface grammars can express complex interfaces that involve both dataflow and control-flow constraints, writing such grammars manually requires a surprisingly large amount of boilerplate code. Crafting the appropriate data structures, verifying the result and extracting the data, even for one operation, requires as much code as the entire interface grammar. Moreover, parameters such as items and token refer to actual elements inside doc, but the grammar in Figure 3 offers no way of actually specifying how the document and its parts are structured or related. To alleviate this difficulty, we developed a tool that uses type information to automatically translate the data structures associated with a WSDL specification into an interface grammar, without user input. 3.1 Translation from XML Schema to Interface Grammars A WSDL specification is a list of exposed operations along with the type of the parameters and return values. It encodes all types using XML Schema. Since XML Schema itself is verbose, we use the Model Schema Language (MSL) formalism [10], which encodes XML Schema in a more compact form. More precisely, we define a simplified version of MSL that handles all the portions of XML Schema we found necessary in our case studies: g b t[g0 ] g1 {m, n} g1,..., g k g1... g k (1) Here g, g 0, g 1,...,g k are all MSL types; b is a basic data type such as Boolean, integer, or string; t is a tag; and m and n are natural numbers such that m n (n may also be ). The MSL type expressions are interpreted as follows: g b specifies a basic type b; g t[g 0 ] specifies the sub-element t of g, whose contents are described by the type expression g 0 ; g g 1 {m, n}, where n, specifies an array of g 1 s with at least m elements and at most n elements; g g 1 {m, } specifies 6 an unbounded array of g 1 s with at least m elements; g g 1,..., g k specifies an ordered sequence, with each of the g i s listed one after the other; and g g 1... g k specifies choice, where g is one of the g i s. We denote the language of type expressions generated by Equation (1) to be X ML. For example, the type for the DoExpressCheckoutPaymentResponse message (Figure 2c) is the following: Token[string], PaymentInfo[ TransactionID[string], GrossAmount[int], PendingReason[string]] As a more complex example, the SetExpressCheckoutRequest message (Figure 2a) is of the following type: Token[string]{0, 1}, PaymentDetails[ OrderTotal[int], PaymentDetailsItems[ PaymentDetailsItem[ Name[string]{0, 1}, Number[string]{0, 1}, Quantity[int]{0, 1}, Amount[int]{0, 1}, ]{1, } ]{0, }, PaymentAction[string]{0, 1}] These type expressions can be used to generate XML documents. However, to communicate with a SOAP server, we chose to use Apache Axis, a library that serializes Java objects into XML. Accordingly, we create Java objects from XML type expressions, and do so in the same way that Axis maps WSDL to Java objects. XML Schema and the Java type system are very different and, hence, mapping from one to the other is not trivial. However, since such a mapping is already provided by Axis, all we have to do is the follow the same mapping that Axis uses: 1. g b is mapped to a Java basic type when possible (for example, with Booleans or strings). Because XML Schema integers are unbounded and Java integers are not, we must use a specialized Java object rather than native integers. 2. g t[g 0 ] is mapped to a new Java class whose name is the concatenation of the current name and t; this class contains the data in g 0, and will be set to the t field in the current object. 3. g g 1 {0, 1} is mapped to either null or the type mapped by g g g 1 {m, n} is mapped to a Java array of the type mapped by g g g 1,...,g k is mapped to a new Java class that contains each of the g i s as fields. 6. g g 1... g k is mapped to a new Java interface that each of the g i s must implement. 7 The rules for the WSDL to interface grammar translation are shown in Figure 4. The translation is defined by the function p, which uses the auxiliary functions r (which gives unique names for type expressions suitable for use in grammar nonterminals) and t (which gives the name of the new Java class created in the Axis mapping of g t[g 0 ]). By applying p g to an XML Schema type expression g, we compute several grammar rules to create Java object graphs for all possible instances of the type expression g. The start symbol for the generated interface grammar is r g. p : X ML Prod r : X ML NT t : X ML Type p g = boolean = ( ) r g (x) x = true, r g (x) x = false (2) ( r g (x) x = 0, ) p g = int = r g (x) r g (x); x = x + 1 (3) ( r g (x) x = , ) p g = string = r g (x) r g (x); x = x c for every c (4) p g = {c 1,..., c n} = r g (x) x = c i for every c i (5) p g = t[g ] j ff r g (x) if (x null) x = newt g ; = r g p g (y); x.t = y (6) ( ) r g (x) x = null, p g = g {0, 1} = r g (x) r g (x), p g (7) ( r g (x) x = [], ) p g = g {0, } = r g (x) r g (y);r g (x); x = x y p g (8) 8 9 r g (x) x = [], r g (x) r g (y); x = [y], = p g = g {0, n} =... p g (9) : r g (x) r g (y 1);... ;r g (y n); ; x = [y 1,..., y n] p g = g {m, n} j r g (x) r g (y = 1);... ;r g ff (y m); r g (x); x = [y 1,..., y m] x (10) p g p g where g g {0, n m} k[ p g = g 1,..., g k = {r g (x) r g 1 (x);... ;r g k (x)} p g i (11) i=1 k[ p g = g 1... g k = {r g (x) r g i (x)} p g i (12) i=1 For a nonterminal g, p g is the set of associated grammar rules, r g is a unique name suitable for a grammar nonterminal, t g is the unique Java type for that position in the XML Schema grammar, and x and y designate an XML document or subdocument. Fig. 4: MSL to interface grammar translation rules Rule (2) translates Boolean types by simply enumerating both possible values. Calling r g (x) with an uninitialized variable x will set x to either true or 8 false. Rule (3) translates integer numbers to a Java instance by starting at 0 and executin
Search
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks