国部酒城礼品(福建)有限公司出品属白.ppt

CS290C FormalModelsforWebSoftwareLectures11and12 FormalModelingandVerificationofWebServices OrchestrationandChoreographyInstructor TevfikBultan WebRevolution SharinginformationusingInternethasbeenabigsuccessKeycomponentsInternetInternetprotocolssuchasTCP IPWWWandHTTPHTMLformatWebbrowsersSharinginformationusingthehttp html browserframeworkhasbeensuccessfulinalotofapplicationsListyourfavoritewebsiteshere WhatNext Thereareapplicationswherehttp html browserframeworkdoesnotworkBusinesstobusinessapplicationsHTMLisdevelopedfordisplayinginformationinawaythatisunderstandableforhumansHTMLisnotveryusefulinhelpingcomputersunderstandthecontentBasicQuestionCanweextendtheinteractionandsharingthatWWWcreatedamonghumanstointeractionandsharingamongserviceswheretheservicesshareinformationandcollaborateusingtheInternet MoreQuestions Whatshouldbetheformatthattheservicessharetheinformation Howwilltheinformationformatbedefined Whatprotocolwillthecomputersusetosendandreceiveinformation Howcanacomputerfindoutabouttheinformationprovidedbyanothercomputer Howcanwedescribetheinteractionamongmultiplecomputers SomeProposedAnswers Whatshouldbetheformatthattheservicessharetheinformation XMLHowwilltheinformationformatbedefined XMLSchemaWhatprotocolwilltheservicesusetosendandreceiveinformation SOAPHowcanaservicefindoutabouttheinformationprovidedbyanotherservice WSDL UDDIHowcanwedescribetheinteractionamongmultipleservices BPEL WS CDL WebServicesStandardsStack Data Type Service Orchestration Protocol WS BPEL WebServiceStandards ImplementationPlatforms Microsoft Net SunJ2EE WSDL UDDI SOAP XMLSchema XML WS CDL Choreography WhatareWebServices Webservicescanbedescribedaswebaccessiblesoftwarethatprovideinterfacesforservicedescription discovery andinteraction WebServices Challenges WebservicesimplementedusingdifferentimplementationplatformsshouldbeabletointeractwitheachotherTherearedifferentimplementationplatformssuchas NetorJ2EEItshouldbepossibletomodifyanexistingwebservicewithoutmodifyingotherservicesthatinteractwithitWebservicesshouldbeabletoleratepausesinavailabilityofotherservicesandslowdatatransmission WebServices Challenges Can twesolvethesechallengeswithexistingtechnologies ExistingtechnologiesfordistributedcomputingsuchasCORBAandRMIrequiretightcouplingamongapplicationsItisnotpossibletospecifyinteractionsamongservicesusingstatelessprotocols WebServices Characteristics Webservicesaddressthesechallengeswiththefollowingcommoncharacteristics StandardizeddatatransmissionviaXMLLoosecouplingamonginteractingwebservicesthroughstandardizedinterfacesMessagebasedcommunication WebServices TheWorldWideWebConsortium W3C definesaWebserviceas asoftwaresystemdesignedtosupportinteroperablemachine to machineinteractionoveranetwork Thebasicarchitecture ServiceRequester ServiceProvider ServiceBroker Register Search Request Response WebServicesStandardsStack Data Type Service Registry Protocol UniversalDescription Discovery Integration UDDI WebServicesDescriptionLanguage WSDL SimpleObjectAccessProtocol SOAP XMLSchema XSD ExtensibleMarkupLanguage XML ServiceRequester ServiceProvider ServiceBroker Register Search Request Response SOAP WSDL WSDL UDDI WebServicesCharacteristics Goals InteroperabilityPlatformindependent NET J2EE ServiceinteractionsacrossorganizationalboundariesLoosecouplingStandardizeddatatransmissionviaXMLInteractionbasedonstandardizedinterfacessuchasWSDLCommunicationviamessagesSynchronousandasynchronousmessaging BasicUsageofWebServices Whatwehavesofarsupportsbasicclient serverstyleinteractionsExample AmazonE CommerceWebService AWS ECS AWS ECSWSDLspecificationlists40operationsthatprovidedifferingwaysofbrowsingAmazon sproductdatabasesuchasItemSearch CartCreate CartAdd CartModify CartGet CartClearBasedontheAWS ECSWSDLspecificationonecanimplementclientsthatinteractwithAWS ECS ServiceRequester ServiceProvider Request Response SOAP WSDL Client Server ComposingServices Canthisframeworksupportmorethanbasicclient serverstyleinteractions Canwecomposeasetofservicestoconstructanewservice Forexample Ifwearebuildingabookstoreservice wemaywanttousebothAmazon sserviceandBarnes Noble sserviceinordertogetbetterpricesAnother well known example Atravelagencyservicethatusesotherservices suchasflightreservation hotelreservation andcarrentalservices tohelpcustomersbooktheirtrips ComposingServices Twodimensions DefineanexecutableprocessthatinteractswithexistingservicesandexecutestheminaparticularorderandcombinestheresultstoachieveanewgoalOrchestration FromatomicservicestostatefulservicesSpecifyhowtheindividualservicesshouldinteractwitheachother FindorconstructindividualservicesthatfollowthisinteractionspecificationChoreography Globalspecificationofinteractionsamongservices Orchestrationvs Choreography Orchestration CentralcontrolofthebehaviorofadistributedsystemLikeaconductorconductinganorchestraConductorisinchargeduringtheperformanceOrchestrationspecifiesanexecutableprocess identifyingwhenandhowthatprocessshouldinteractwithotherservicesOrchestrationisusedtospecifythecontrolflowofacompositewebservice asopposedtoanatomicwebservicethatdoesnotinteractwithanyotherservice Orchestrationvs Choreography Choreography SpecificationofthebehaviorofadistributedsystemwithoutcentralizedcontrolChoreographerspecifiesthebehaviorofthedancingteamChoreographerisnotpresentduringtheexecutionAchoreographyspecifieshowtheservicesshouldinteractItspecifiesthelegalsequencesofmessagesexchangedamongindividualservices peers ItisnotnecessarilyexecutableAchoreographycanberealizedbywritinganorchestrationforeachpeerinvolvedinthechoreographyChoreographyasglobalbehaviorspecificationOrchestrationaslocalbehaviorspecificationthatrealizestheglobalspecification OrchestrationwithWS BPEL WebServicesBusinessProcessExecutionLanguage WS BPEL isanorchestrationlanguageAWS BPELspecificationdescribestheexecutionlogicusingbasicandstructuredactivitiesBasicactivities RECEIVE REPLY INVOKE ASSIGN THROW TERMINATE WAIT EMPTYRECEIVE REPLY INVOKEStructuredactivities SEQUENCE SWITCH WHILE PICK FLOW SCOPE COMPENSATEWS BPELsupportsmessaging RECEIVE REPLY INVOKE andmulti threading FLOW ChoreographywithWS CDL WebServicesChoreographyDescriptionLanguage WS CDL WS CDLspecificationsdescribe peer to peercollaborationsofWebServicesparticipantsbydefining fromaglobalviewpoint theircommonandcomplementaryobservablebehavior whereorderedmessageexchangesresultinaccomplishingacommonbusinessgoal AWS CDLspecificationdescribestheinteractionorderingamongasetofpeersusingbasicandstructuredactivitiesBasicactivities INTERACTION PERFORM ASSIGN SILENTACTION NOACTIONStructuredactivities SEQUENCE PARALLEL CHOICE PICK FLOW SCOPE COMPENSATE WebServicesStandardsStack Data Type Service Orchestration Protocol WebServicesBusinessProcessExecutionLanguage WS BPEL WebServicesDescriptionLanguage WSDL SimpleObjectAccessProtocol SOAP XMLSchema XSD ExtensibleMarkupLanguage XML AtomicService AtomicService OrchestratedService SOAP WSDL WSDL Choreography WebServicesChoreographyDescriptionLanguage WS CDL WS BPEL OrchestratedService WS BPEL SOAP SOAP SOAP SOAP WS CDL AnExample StockAnalysisService Thestockanalysisserviceinvolves threepeersInvestor StockBrokerFirm andResearchDepartmentHereishowthestockanalysisserviceoperates InvestorinitiatesthestockanalysisservicebysendingaregistermessagetotheStockBrokerFirmTheStockBrokerFirmmayacceptorrejecttheregistrationIftheregistrationisaccepted theStockBrokerFirmsendsananalysisrequesttotheResearchDepartment AnExample StockAnalysisService ResearchDepartmentsendstheresultsoftheanalysisdirectlytotheInvestorasareportAfterreceivingareporttheInvestorcaneithersendanacktotheStockBrokerFirmorcanceltheserviceThen theStockBrokerFirmeithersendsthebillfortheservicestotheInvestor orcontinuestheservicewithanotheranalysisrequest AnExample StockAnalysisService SAS registerack cancel accept reject bill request terminate report Investor Inv ResearchDept RD StockBroker SB SASisacompositeservicethatcontainsthreeindividualservices IBlink register IBlink reject IBlink accept RIlink report IBlink ack IBlink cancel RIlink bill RIlink bill Investor reject accept bill Callbackport IBlink register IBlink reject IBlink accept BRlink request IBlink ack IBlink cancel RIlink bill RIlink bill StockBrokerFirm register cancel ServicePort request DelegatePort ServicePort OutputPort RIlink BRlink IBlink BRlink request RIlink report ResearchDept ack StockAnalysisService StockAnalysisService InthefollowingslidesIwilldiscusshowdifferentpartsofthestockanalysisservicecanbedescribedusingemergingwebservicestandardsMessagecontents XMLMessagetype XMLSchemaMessageports WSDLBehavior BPEL XML eXtensibleMarkupLanguage XMLisamarkuplanguagelikeHTMLSimilartoHTML XMLtagsarewrittenasfollowedbyHTMLvs XMLInHTML tagsareusedtodescribetheappearanceofthedata InXML tagsareusedtodescribethecontentofthedataratherthantheappearanceXMLdocumentscanbemodeledastreeswhereeachinternalnodecorrespondstoatagandleafnodescorrespondtobasictypes AnXMLDocumentandItsTree 1234AAAABBBB56 XMLSchema XMLprovidesastandardwaytoexchangedataovertheinternet However thepartieswhichexchangeXMLdocumentsstillhavetoagreeonthetypeofthedatawhatarethetagsthatwillappearinthedocument inwhatorder etc XMLSchemaisalanguagefordefiningXMLdatatypes MSL ModelSchemaLanguage MSL ModelSchemaLanguage isacompactformalmodellanguagewhichcapturesmostfeaturesofXMLSchemaBasicMSLsyntaxg b t g g m n g g g g g ggisanXMLtype i e anMSLtypeexpression istheemptysequencebisabasictypesuchasstring boolean int etc tisatagmandnarepositiveintegers areMSLtypeconstructors MSLSemantics t g denotesatypewithrootnodelabeledtwithchildrenoftypegg m n denotesasequenceofsizeatleastmandatmostnwhereeachmemberisoftypegg1 g2denotesanorderedsequencewherethefirstmemberisoftypeg1andthesecondmemberisoftypeg2g1 g2denotesanunorderedsequencewhereonememberisoftypeg1andtheothermemberisoftypeg2g gdenotesachoicebetweentypeg1andtypeg2 i e eithertypeg1ortypeg2 butnotboth AnMSLTypeDeclarationandanInstance Register investorID xsd int requestList stockID xsd string 1 50 payment creditCardNum xsd int accountNum xsd int 1234AAAABBBB56 AnMSLTypeDeclarationandanInstance Register investorID 1234 requestList stockID AAAA stockID BBBB payment accountNum 56 MSLcanalsobeusedasacompactlanguageforspecifyingdatainstances XPath InordertowritespecificationsorprogramsthatmanipulateXMLdocumentsweneed anexpressionlanguagetoaccessvaluesandnodesinXMLdocumentsXPathisalanguageforwritingexpressions queries thatnavigatethroughXMLtreesandreturnasetofanswernodesAnXPathquerydefinesafunctionwhichtakesandXMLtreeandacontextnode inthesametree asinputandreturnsasetofnodes inthesametree asoutput XPathSyntax BasicXPathsyntax q b t q q q q q q q q q exp qisanXPathqueryexpdenotesapredicateonbasictypes i e ontheleafnodesoftheXMLtreebdenotesabasictypesuchasstring boolean int etc tdenotesatag XPathSemantics GivenanXMLtreeandanodenasacontextnode returnsn returnstheparentofnGivenanXMLtreeandasetofnodes returnsallthenodesbreturnsthenodesthatareofbasictypebtreturnsthenodeswhicharelabeledwithtagt XPathSemanticsContd Startingatthecontextnode qreturnsthenodesthatmatchq qreturnsthenodesthatmatchqstartingatanydescendantq1 q2returnseachnodewhichmatchesq2startingatachildofanodewhichmatchesq1q1 q2returnseachnodewhichmatchesq2startingatadescendantofanodewhichmatchesq1q1 q2 appliesq2tothechildrenofthenodeswhichmatchq1q exp returnsthenodesthatmatchqandforchildrenofwhichtheexpressionexpevaluatestotrue ExampleXPathQueries payment returnsthenodelabeledaccountNum Register requestList stockID stringreturnsthenodeslabeledAAAAandBBBB stockID string AAAA stringreturnsthenodelabeledAAAA int 100 intreturnsthenodelabeled1234 WSDL WebServicesDescriptionLanguage WSDLisanXML basedlanguageusedtodeclareandpublishthepublicinterfacesofWebservicesWiththeWSDLdescription theinvokerofaparticularwebservicecanlearnaboutthewebservicelocationthecallssupportedbythewebservicetheformatofthemessagestoplaceacallWSDLusesXMLSchematodefinemessagetypesContentsofthemessagesareXMLdocumentsWSDLspecificationsdeclaremessageportsinputports outputportsetc WSDLExample DeclaringMessageTypes WSDLExample DeclaringMessageTypes Thefollowingisaparagraphtakenfrombroker xsdusedintheRegisterdeclarationinthepreviousslide WSDLExample DeclaringMessagePorts IBlink register IBlink reject IBlink accept RIlink report IBlink ack IBlink cancel RIlink bill RIlink bill Investor reject accept bill Callbackport IBlink register IBlink reject IBlink accept BRlink request IBlink ack IBlink cancel RIlink bill RIlink bill StockBrokerFirm register cancel ServicePort request DelegatePort ServicePort OutputPort RIlink BRlink IBlink BRlink request RIlink report ResearchDept ack StockAnalysisService BPEL BusinessProcessExecutionLanguage ThesimplefunctioncallmodelemployedbyWSDLmakesithardtocapturelongrunningcomplexcompositewebservicessuchasthestockanalysisservicetheorderingbetweenthecallscannotbeexpressedThecontrolflow i e thebehavior ofthepeersofthestockanalysisservicecanbespecifiedusingBPEL BPEL PartnerLinks IntheBPELspecification firstasetofpartner linksaredeclaredThepartnerlinksfortheexampleinthestockanalysisservicearenamedIBLink BRLinkandRLinkEachpartnerlinkconnectsapairofportdeclaredintheWSDLspecificationAfterthedeclarationofthepartnerlinks BPELspecificationforeachpeerincludesthecontrolflowofthecorrespondingpeerwiththeassociatedreceiveandsendoperationsthroughthepartnerlinksandWSDLports BPEL PartnerLinks BPEL ControlFlow BPELborrowsmanycontrolstructuresfromcommonprogramminglanguages suchassequence while switch etc TheatomicoperationsinBPELareinvoke receive andreplyusedforsendingandreceivingmessages andassignusedforupdatingvaluesofthevariables Sinceassignmentsareconductedoncomplextypevariables WSDLmessagesdeclaredasXMLSchematypes BPELsupportsXPathexpressionstoidentifythesourcesandthedestinationsoftheassignmentsstatements BPEL ControlFlow FormalModelingandVerificationofWebservices TherehasbeenalotofworkonmodelingandverificationofwebservicesTheseeffortsmostlyfocusedonanalyzingcompositeservicesspecifiedusingorchestrationandchoreographylanguagesForexample canweformallymodelagivenBPELspecificationandautomaticallyverifyitspropertiesIwillgiveanoverviewofatoolwebuiltforBPELverificationcalledWebServiceAnalysisTool WSAT BPELtoGFSA Guardedautomata GFSAtoPromela boundedqueue BPEL WebServices Promela SynchronizabilityAnalysis GFSAtoPromela synchronouscommunication IntermediateRepresentation ConversationProtocol FrontEnd RealizabilityAnalysis Guardedautomaton skip GFSAparser success fail GFSAtoPromela singleprocess nocommunication success fail Analysis BackEnd bottom up top down VerificationLanguages WebServiceAnalysisTool WSAT Fu Bultan SuCAV 04 http www cs ucsb edu su WSAT BPELtoStateMachineTranslation EachatomicBPELactivitiescanbetranslatedtoastatemachinesingleentry singleexit andmayhaveseveralexceptionexitsTransitionshaveguards extendedstatemachine apprvInfo accept yes approve In request approve In BPELtoStateMachineTranslation handler1 approve In approve Out loanfault loanfault approve In request BPELtoStateMachineTranslation Controlflowconstructscanbehandledbycomposingstatemachines act1 act2 fault2 fault1 act1 act2 product BPELtoStateMachineTranslation WecantranslateBPELspecificationstoastatemachinerepresentationbyrecursivelyapplyingtranslationruleslikewedescribeaboveHowever BPELspecificationsdonotonlyhavecontrolflowconstructstheycanalsocontainbranchconditionsandassignmentstatementsexpressedusingXpathSowehavetouseanextendedstatemachinerepresentationwhichkeepsthebranchconditions assignments etc GuardedAutomataModel GuardedautomatamodelisanextendedstatemachinemodelthatusesXMLmessages MSLandXPathUsesMSLfordeclaringmessagetypesMSL ModelSchemaLanguage isacompactformalmodellanguagewhichcapturescorefeaturesofXMLSchemaUsesXPathexpressionsforguardsXPathisalanguageforwritingexpressions queries thatnavigatethroughXMLtreesandreturnasetofanswernodes TranslatingGuardedAutomatatoPromela WeusedtheSPINmodelcheckertoverifythepropertiesofconversationsSPINisafinitestatemodelcheckerwerestrictedXMLmessagecontentstofinitedomainsWetranslateguardedautomatamodelstoPromela inputlanguageoftheSPINmodelchecker First translateMSLtypedeclarationstoPromelatypedeclarationsThen translateXPathexpressionstoPromelacode MappingMSLtypestoPromela BasictypesintegerandbooleantypesaremappedtoPromelabasictypesintandboolWeonlyallowconstantstringvaluesandstringsaremappedtoenumeratedtype mtype inPromelaOthertypeconstructorsarehandledusingstructuredtypes declaredusingtypedef inPromelaorarrays MappingMSLtypeconstructorstoPromela t g istranslatedtoatypedefdeclarationg m n istranslatedtoanarraydeclarationg1 g2istranslatedtoasequenceoftypedeclarationsg1 g2istranslatedtoasequenceoftypedeclarationsandanenumeratedvariablewhichisusedtorecordwhichtypeischoseng1 g2isnothandled Wedonothandleunorderedtypesequence itcancausestate spaceexplosion Example Register investorID string requestList stockID int 1 3 payment creditCardNum int accountNum int typedeft1 investorID mtypestringvalue typedeft2 stockID intintvalue typedeft3 requestList t2 stockIDstockID 3 intstockID occ typedeft4 accountNum intintvalue typedeft5 creditCard intintvalue mtype m accountNum m creditCard typedeft6 payment t4 accountNumaccountNum t5 creditCardcreditCard mtypechoice typedefRegister t1 investorIDinvestorID t3 requestListrequestList t6 paymentpayment XPathtoPromela GeneratecodethatevaluatestheXPathexpression Fu Bultan SuISSTA 04 TraversetheXPathexpressionfromlefttorightCodegeneratedineachstepisinsertedintotheBLANKspacesleftinthecodefromthepreviousstepAtreerepresentationoftheMSLtypeisusedtokeeptrackofthecontextofthegeneratedcodeUsestwodatastructuresTypetreeshowsthestructureofthecorrespondingMSLtypeAbstractstatementswhicharemappedtoPromelacode IF v if v BLANK else skipfi v l 1do vBLANKv else breakod BLANK FOR v l h EMPTY INC v SET v a v v a Statement PromelaCode investorID Register string requestList int payment creditCard int stockID idx i1 accountNum int 1 2 3 4 10 8 7 5 6 9 11 Register investorID string requestList stockID int 1 3 payment creditCardNum int accoun