DOC PREVIEW
A Tool for Formal Analysis

This preview shows page 1-2-16-17-18-33-34 out of 34 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 34 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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 protocolConversationProtocolAB:msg1BA:msg2BC:msg3 C B:msg4BC: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?msg6BA: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


A Tool for Formal Analysis

Download A Tool for Formal Analysis
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view A Tool for Formal Analysis and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view A Tool for Formal Analysis 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?