WSAT A Tool for Formal Analysis of Web ServicesWeb ServicesChallenges in Verification of Web ServicesOutlineComposite Web ServicesConversation ProtocolsSlide 7Top-Down ApproachRealizability ProblemAnother Non-Realizable ProtocolYet Another Non-Realizable ProtocolRealizability ProblemBottom-Up ApproachThree Examples, Example 1Example 2Example 3Three ExamplesSynchronizability AnalysisAre These Conditions Too Restrictive?Web Service Analysis Tool (WSAT)Guarded Automata ModelSAS Guarded AutomataAn XML Document and Its TreeAn MSL Type Declaration and an InstanceMSL to Promela ExampleXPath ExpressionsXPath to PromelaSlide 28Slide 29Model Checking Using PromelaRelated WorkSlide 32Future WorkSlide 34WSATA Tool for Formal Analysis of Web ServicesXiang Fu Tevfik Bultan Jianwen SuDepartment of Computer ScienceUniversity of California, Santa Barbara{fuxiang,bultan,su}@cs.ucsb.eduWeb Services•Loosely coupled, interaction through standardized interfaces•Standardized data transmission via XML•Asynchronous messaging•Platform independent (.NET, J2EE)DataTypeService CompositionMessageBPEL4WSWeb Service StandardsImplementation PlatformsMicrosoft .Net, Sun J2EEWSDLSOAPXML SchemaXMLWSCIInteractionChallenges in Verification of Web Services•Distributed nature, no central control–How do we model the global behavior?–How do we specify the global properties?•Asynchronous messaging introduces undecidability in analysis–How do we check the global behavior?–How do we enforce the global behavior?•XML data manipulation–How do we specify XML messages?–How do we verify properties related to data?Outline•Web Service Composition Model –Conversations: Capturing Global Behaviors•Top-Down vs. Bottom-Up Specification and Verification–Realizability vs. Synchronizability•XML messaging–MSL, XPath–Translation to Promela•Web Service Analysis Tool•Conclusions and Future Work!register?reject ?accept?report!ack!cancel?bill?billInvestor?register!reject!accept!request?ack?cancel!bill!billStock Broker Firm?request?terminateResearch Dept.!reportaccreqregrepackComposite Web Services!terminatebilterWatcherrepaccbilreg ackreq terConversation Protocols1234657 810912 11registerrejectterminateacceptrequestreportackrequestreportackcancelbill cancelbillterminate•A conversation is a sequence of messages the watcher sees during an execution [Bultan, Fu, Hull, Su WWW’03]•Conversation Protocol: An automaton that accepts the desired conversation setSAS conversation protocolConversationProtocolAB:msg1BA:msg2BC:msg3 C B:msg4BC:msg5G(msg1 F(msg3 msg5))?LTL property!msg1?msg2Peer A?msg1!msg2!msg5!msg3?msg4Peer B?msg3!msg4Peer CPeer A Peer B Peer Cmsg1msg2,msg6msg3,msg5msg4ConversationSchemaInputQueue...Virtual Watcher?msg6BA:msg6!msg6?msg5G(msg1 F(msg3 msg5))?LTL propertyComposite Web ServiceTop-Down Approach•Conversation protocol specifies the global communication behavior–How do we implement the peers?•Project the global protocol to each peer–By dropping unrelated messages for each peerAre there conditions which ensure the equivalence?Conversations generated by the composed behavior of the projected servicesConversations specified by the conversation protocol?Realizability Problem•Not all conversation protocols are realizable!A B: m1C D: m2Conversation protocol!m1?m1!m2?m2Peer A Peer B Peer C Peer DConversation “m2 m1m2 m1” will be generated by any legal peer implementation which follows the protocolProjection of the conversation protocol to the peersThis protocol fails Lossless join conditionAnother Non-Realizable Protocolm3m1m2m1m2m3A B: m1A C: m3B A: m2ABCm1m2 m3WatcherA BCB A, CB A: m2A B: m1This protocol fails Autonomous conditionYet Another Non-Realizable Protocolm1m2m1m2A B: m1C A: m2ABCm1m2WatcherA BCThis protocol fails Synchronous compatible conditionRealizability Problem •Three sufficient conditions for realizability [Fu, Bultan, Su, CIAA’03, TCS]–Lossless join: Conversation set should be equivalent to the join of its projections to each peer–Synchronous compatible: When the projections of the conversation protocol are executed with synchronous communication semantics, there should not be a state where a peer is ready to send a message while the corresponding receiver is not ready to receive–Autonomous: Each peer should be able to make a deterministic decision on whether to send or to receive or to terminateBottom-Up Approach•We know that analyzing conversations of composite web services is difficult due to asynchronous communication•The question is, can we identify composite web services where asynchronous communication does not create a problem?Three Examples, Example 1?r1!a1!a2?r2?erequester server!r2?a1?a2!e!r1•Conversation set is regular: (rConversation set is regular: (r11aa11 | r | r22aa22)* e)* e•During all the executions queues are boundedr1, r2a1, a2eExample 2!r1!r2?a1?a2!e?r1!a1!a2?r2?er1, r2a1, a2requester servere•Conversation set is not regularConversation set is not regular•Queues are not boundedExample 3r1, r2a1, a2requester servere!r1!r!r2?a!e?r1?r !a?e?r2•Conversation set is regular: (rConversation set is regular: (r11 | r | r22 | r a)* e | r a)* e•Queues are not boundedThree Examplesqueue length# of states in thousands•Verification of Examples 2 and 3 are difficult even if we bound the queue length•How can we distinguish Examples 1 and 3 (with regular conversation sets) from 2?–Synchronizability AnalysisSynchronizability Analysis•A composite web service is synchronizable, if its conversation set does not change when asynchronous communication is replaced with synchronous communication•A composite web service is synchronizable, if it satisfies the synchronous compatible and autonomous conditions[Fu, Bultan, Su WWW’04]Are These Conditions Too Restrictive?Problem Set Size Synchronizable?Source Name #msg #states #trans.ISSTA’04 SAS 9 12 15 yesIBM Conv.SupportProjectCvSetup 4 4 4 yesMetaConv 4 4 6 noChat 2 4 5 yesBuy 5 5 6 yesHaggle 8 5 8 noAMAB 8 10 15 yesBPELspecshipping 2 3 3 yesLoan 6 6 6 yesAuction 9 9 10 yesCollaxa.comStarLoan 6 7 7 yesCauction 5 7 6 yesBPEL toGFSAGuardedautomataGFSA to Promela (bounded queue) BPELWebServicesPromelaSynchronizability AnalysisGFSA to Promela(synchronouscommunication)IntermediateRepresentationConversationProtocolFront EndRealizability AnalysisGuardedautomatonskipGFSAparsersuccessfailGFSA to
or
We will never post anything without your permission.
Don't have an account? Sign up