Biological Network Analysis
Biological Network Analysis CIS 6930
Popular in Course
Popular in Computer Information Systems
This 49 page Class Notes was uploaded by Mabel Smitham PhD on Wednesday September 23, 2015. The Class Notes belongs to CIS 6930 at University of South Florida taught by Staff in Fall. Since its upload, it has received 12 views. For similar materials see /class/212608/cis-6930-university-of-south-florida in Computer Information Systems at University of South Florida.
Reviews for Biological Network Analysis
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/23/15
CIS 69304930 Computer Aided Veri cation Tem poral Logics Hao Zhe Dept of Computer Science amp Eng Univ of South Florida Laue mm m 5mg my ulswsu Semi A mes IWWGN mm kr Wm Mama ems Temporal Logics A formalism to describes properties of paths in the model of reactive systems First order logic augmented with temporal operators Time is implicit Explicit in realtime temporal logics There exist different temporal logics With different View of underlying computation CTLquotlt CTL Views computation of a system as a tree System can move into different future LTL Views computation of a system as a set of paths System has only one direction into the future Models of Computations Computation tree State transition graph Paths Kripke Structure Computational Tree Logic CTLquot To describe paths from a given state 0 Path quanti ers A for all computation paths from a state E for some computation paths from a state 0 Linear temporal operators describe properties along a path Gp p holds in every state on the path Fp p holds in some state on the path Xp p holds in the second state of the path pUq p holds until q holds in some state on the path qu similar to U but q does not need to hold State and Path Formulas Path formulas hold along a path If f is a state formula it is also a path formula If f and g are path formulas so are boolean combinations off andgXfFfG andeg State formulas hold at a state If p is an atomic proposition then p is a state formula If f and g are state formulas so are boolean combinations off and g If f is a path formula A f and E f are state formulas CTLquotlt formuals are state formulas generated by the above rules Semantics Path Formulas De ned Wrt a Kripke structure M o If f is a path formula My I f means f holds along path 7r 0 De nitions M 7r I f lt gt f is a state formula 5 is the first state of M s I f holds if p is an atomic proposition and p e Ls M 7r I f lt gt f is a path formula and M 7r I f does not hold M 7rfvg lt gtfandg arepathformulasandM s f orM sf M 7rng lt gtfandg arepathformulasandM s f andM sf M 7rXf lt gtfis apath formula andM 7r1f M 7rFf lt gtfis apath formula andM 7rk ffor somekZO M 7r G f lt gtfis a path formula and M 7rk ffor all k 2 0 M 7r f U g lt gt Semantics State Formulas De ned Wrt a Kripke structure M o If f is a state formula M s f means f holds at state s of M 0 De nitions M s I p lt gt if p is an atomic proposition and p E Ls M s f lt gtM sfdoesnothold Msfvg lt gtMsforMsf Msfg lt gtMsfandMsf M s A f lt gt f is a path formulas and for all paths 7r from s such that M 77 I f M s I E f lt gt f is a path formula and there is a path 7r from s such that M 77 I f Equivalences Not all operators are essential to express a property ngE fv g AfE E f GfE F at FfE true Uf FfvgEFfFg What about Ff g E Ff Fg GngEGfGg What about Gf g E va Gg ngE gU fA gD AFg CTL and LTL CTLquotlt is more expressive but expensive for veri cation Two useful sublogics of CTL CTL and LTL CTL is a restricted subset of CTLquotlt Where temporal operators must be immediately preceded by a path quanti er Basic operators AG AF AX AU EG EF EX EU Example AG EF f LTL consists of formulas of the form Af de ned as follows If p is an atomic formula the p is a path formula if f and g are path formulas so are boolean combinations of f and g Xf Ff Gf ande g Example A FG f Interpretation of CTL Operators AG f is true EG f is true Interpretation of CTL Operators AF f is true EF f is true Interpretation of CTL Operators AX f is true EX f is true Interpretation of CTL Operators Af U g is true Ef U g is true A Sufficient Set of CTL Operators Any CTL formulas can be expressed using EX EG and EU AX f EX f AGf EF f E true U f AF f EG f A fU g EG g A E g U fA g What does AGAF f mean LTL Semantics Example S0 S2 S a 3 M sop Aq MS0XV M S0G IpI M Sol CFP A Sufficient Set of LTL Operators U X R X or W X is suf cient GfE FIf XfEX f ngE fU g ngEfWgAFg FfEtrueUf Examples GFf and FGf CTLquot CTL and LTL CTLquotlt CTL formula speci es a set of states A LTL formula specifies a set of paths 39 AFG f is not expressible in CTL AGEF f is not expressible in LTL Safety and Liveness Properties 0 Safety nothing bad should happen Liveness something good eventually happens 0 Example a mutual exclusion element U1 gt QM U2 gt 92 Mutual Exclusion r1 a1 r2 32 Fairness Fairness means certain properties happen in nitely often during compuation An arbiter cannot ignore some requests forever A communication channel cannot lose message all the time Models may contain unfair computations Nondeterministic models of physical computating systems Wrong implementations of fairness requirements Fairness constraints eliminate the unfair computations Unfairness introduced to simplify modeling Fair computations satisfy fairness constraints in nitely often Fair Semantics Fairness constraints are expressed as sets of states that hold in nitely often on computations CTLquotlt semantics with fairness M s Fp lt gt ifthere is a fair path from s andp E Ls M s F A f lt gt f is a path formulas and for all fair paths 7 from s such that M 7239 f M s F E f lt gt f is a path formula and there is a fair path 7 from s such thatM 7239 f CTL will discuss it later LTL fairness can be easily expressed and incorporated with veri cation EXGFporGFpGFq Introduction to SOA and Web Services Federated Distributed Systems Class Nov 8 2006 Content III Motivation III What are Web Services III WS Characteristics III WS Architecture III Web Service Implementation III Research issues Motivation Before III Applications were very specialized Each company had to build them III Applications were very complex and heavy to maintain I Data was maintained by the company III Servers to support applications were neededlocaHy III Writing software became a difficult activity Motivation Today III Modular design is promoted III Legacy systems are stable nobody wants to change code III Small pieces of code are required for many people III Programmers need a way to reuse functionality notjust codequot III Services decomposed on finer grained components III Applications are seen as commodities homogeneous products services Motivation Typical problems IZIHeterogeneous platforms program languages various devices sensors etc IZIDifferent vendors use different data schemas amp formats IZISubsystem providers are typically autonomous and coordination is not easy to undertake or even impossible Motivation Desired Properties III Interface platform independent III Service dynamically located and invoked III Self contained Requirement 9 Need for a common programtoprogram communication model build upon existing and emerging standards Motivation To ensure interoperability to the greatest possible extent we need three fundamental standards Common encoding schema for requests and responses Standardized description language to make metadata widely interpretable Well defined catalog discovery service to find available and suitable WebServices all over the Web Service Oriented Architecture Fundamental concept Service Trading Publish Find Bind Paradigm Publishes Queries data1 wetada ta or servnce Service Requestor Service lt gt Provuder Service Interaction Composing at runtime not on design time What are Web services Web services are loosely coupled contracted components that communicate via XML based i nte rfa ces Schmezer 2002 loosely coupled they can be changed independently platform independent contracted in and output are publicly available components interface encapsulates the code XMLbased interfaces human readable firewall friendly selfdescribing allows for discovery of their functionality Web Service Characteristics Network accessible via standardized XML messaging typically based on H39I39I39P Described using a standard formal XML notion service description gtCovers all the details necessary to invoke the service message formats location etc Interface hides the implementation details gtAllows it to be used independently of the hardware or software platform on which it is implemented Web Service Characteristics Provide interface accessed by another program Fulfill a specific task or set of tasks gtAccessible through the web gtCan be used alone gtCan be used along with other Web Services to fulfill complex tasks gtCan communicate to other web services Web Services Stack Service aw J BPEL E UD Ell WEDL game http ftp MCI quotGP and mum EEWif E iewve quot 39ry Sarvina dasm ption mbbased39 messaging Source wwwibmcom Web Services Architecture Serviceoriented Web Services architecture SOA technology stack Publish 39 Bind Web Services Specification There are three basic specifications forming the basis for stateoftheart WebService technology Simple Object Access Protocol SOAP for a common message processing amp coding Web Service Description Language WSDL as a metadata standard for WebServices Universal Description Discovery and Integration UDDI specifying a catalog discovery service Web Service Description Language WSDL III Issues to think about What services do you offer How can they invoked What information do they need to be executed How is the user providing that information What format is used to send information back ElThe components of a WSDL document I SOAP messages supported requestresponse I Rules for finding the port at which WS is listening the requests I The definition of the service itself WSDL example Currency converter httpllwwwwebservicexneUCurrencyConvertoerfanSDL Microsaft Internet Explorer E HIE Edlt View Favorites Tools Help Bad 39 dquot q T Search Favurites j E 7 Be z uh r67 nw n warn leo ml 1quot 39 v gFormFxll v39l39 Spaces 39 Y 39 quot SEBI d lWEb V GetI now V EV EV 0 Mail V 7 htrpanwwebserwcexrustic AddTab l CDOgIEiCv 60 x p Q M a v if Bookmarksv Elghlodoad 5 Check v Set ngsv w P lei narn quotf 39 r ltwsdpart nan1e quot elementquotfncF 39 gt ltfw5dlmessagegt 39 namequotf 39 r quot2 wsdlzpart nameJr quot elementquotfn 39f 39 gt ltwsdlmessagegt nam quotf 39 ltwsdlpart namequotFromCurrencvquot typequotsstringquot gt ltwsdlpart nan1equotToCurrencyquot typequotsstring gt ltwsdlmessagegt namequotf 39 ltwsdzpart namequotBodyquot elementquottn5doublequot gt q wsdlzmessagegt namequotf ltwsdlpart namequotFrDmCurrencyquot typequotsstringquot gt ltwsdpart namequotTDCurrencyquot typequot5stringquot gt lt39w5dlrnessagegt namequotf 39 ltwsdpart namequotBodyquot elementquottn5doublequot gt ltfwsdlzmessagegt ltwizr llznnrrTvn9 nan1lquotCnrrnncv nnvertnr nanquotgt httD wwwwebservicex netCu rrenchonvertorasmxWSDL I I SOAP example request Currency converter 3 CurrencyEonvertor Web Service Microsoft Internet Explorer 7 Elle Edit ew Favorites Iools elp QEBack v I v 1 Q I Search Favorites lMedia R dress httpI J39wwwwebservicexnetlI39CurrencyConvertorasmxopConversionRate gem Ll gt60 Links A SOAP The following is a sample SDnP request and response The placeholders shown need to be replaced with actual values POST fCurrencyConvertorasmx HTTP11 Host mwehservicexnet Content Type textfxml charsetutf 8 Content Length length summation quothttpIfwwwwehservicexN39ETIComrersionRatequot ltxm1 versionquot1lquot encodingquotutf 8 gt soapmmrelope xmlnsxsiquothttpfmw3org2 lfm5c2hema instancequot mlnsxsdquot ltsoapBodygt ltComrersionRate mnlns httpffwwwwehservioeXllETfquotgt ltFrmnCurrencygtnFA or ALL or DZD or 3R5 or AWE or nun or BSD or Bill or BDT J ltToCurrencygt F or ALL or DZD or 8R5 or mm or MID or BSD or 311 or BDT or ltfConversionRategt lsoapmody ltfsoapEmrelope g Done f It Internet SOAP example response Currency converter Eurrencytonvertor Web Service Microsoft Internet Explorer D E Eile Edit Eiew Favorites Iools Help I QEBack I v a 1 I Search Favorites FMedia I 3 Address httpll39wwwwebservicexnetICurrenq CcunvertorasmxopConversionRate j Go I Links gt I HTTPI11 200 UK Content Type textHull charsetutf 8 Content Length length ltxml versionquot1lquot encodingquotutf 8quot ltsoapEmrelupe xmlnsxsiquothttpffwwww3orgi2 lim50hmna instmcequot Msxsdquothttpflwwwwf ltsuapBudygt ConversionRateRespunse mlnsquothttpIfwwwwehserviceX1TETquotgt ltCnmrersionRat eRe sult duuh1eltfComrersinnRat eRe suit IComrersionRateResponse isoapmody ltfsoapEmrelopegt Ll Ll IE Done I I I Internet A Previewing a Web Service ciick I4Fi v39 far a compiete list of operatiuns Test To test the operation using the HTTP POST protocol click the 39Invoke button Get conversion rate from ane currency to another currency Parameter Differend urreng Code and Names around the world Value FromCLIrrenCy USDV TnCurrency EP El httpllmvwwebrsiervicexinethurrencyConvertorasrnXIConversionRate Microsoft Internet Explorer File Edit View Favorites Tools Help ltxml versionquot10quot encodingquotutf 8quot gt edouble xmlnsquothttpwwwwebserviceXNETquotgt22845ltd0ubegt httDwwwwebservicexnetWSdefaultasox Universal Description Discovery and Integration UDDI Example UDDI registry Microsoft UDDI Business Registry UBR node e Mitrosoft Internet Explorer Eile Edit iew Favorites Iools elp lt2Back w d v I9 a I FaSearch Favorites xPltledia I 39 a a Address hrrnHiiririi mirrn nFl39 39 39 L c r 4 1 n b I J 60 Miaoso Uddl sum Business Registry Node Quick Help UDDIHelp v Go WebseruiceXNET Home Search A Search Currency Convertor Results Explorer An XML Web service uses standard Web protocols t data with one or more applications regardless of h It service is implemented in its native environment I39 E 1 WSbsercex NET details categorizationsJ and access points bindings 3E Walter V Jones service using the tabs below 43 BibleWebservice 13 iif7 Details I Bindings Categories I d i b Details provide the service name and a brief I 35 Fax We serv39ce description The service key is unique and is 53 Stock Quote intended for use in programmatic queries Service Key 37786659DISlf495688db19b5023bc33b en Currency Convertor 41 l D E Done i l i F6 Internet A httD wwwmicrosoftcomwindowsserver2003technoloqiesidmuddidefaultmspx Web Service brokers I K I 0 N mantlan Yum SIM Search strikeirancam Contacl Register Login Marketplace Products Developers P nners Customers News Company Support YourAccoum l l Purchase Publish Search Web Services Buy or Try a Web service Sell your Web service in the Marketplace lAII Categories SF i JTLiLfri39l39 PRCIEJH Milli ilCEL HUT US Address Veri cation 0 Global SMS Pro Well SEWiEES 39 Sales and Use Tax l l sup StrikeIan Launches Super Data Pack New Web services Super Data PBCk l provide 10000 Free hire per month and a single access 3 point to multiple external data sources l 0 DnDemand Web Services for quotquot2 BER Enters DEM Agreement with Strikelrun to Enable Exce39 Add i 539 Front Of ce to Back Office Integration Bring Live Data to Business Users via Microsoft Excel llE SEWHLES 39 Currency Rates o Strikelron39s Marketplace API 038 WordBase Marketing n httbwwwstrikeironcom When are WS a good option III Clientserver applications III Dynamic environment III Modest performance needs III Interoperability is the main concern III Rapid response is not a requirement Work in progress III WS discovery III Business Process Integration BPEL III WSSecurity III Quality of Service QoS III Performance and reliability III Resource Framework WSRF WS Research topics III Semantic WS III Ontologies for WS III Locationbased WS III Automatic WS composition III WS matchmaking III WS modeling III Grid services To think about III Web services infrastructures promise to revolutionize the way people develop software systems III Usually every organization has a team of skilled programmers with an existing business system realistically the best choice is to continue using the same platform III You need more than good tools and standards Discussion SOA and business What Analysts Are Saying About ServiceOriented Architecture F39rirtstle Versicr39 En39ail Tl ia F soe By EDGE SOA will provide the basis for 80 of new development projects Ely 2008 SUAs will enable organizations to increase code reuse by more than was ServiceDriented Architecture 39zquot5l39 is EDA Irr c rte r 7 A1 a By 2010 80 of application software revenue growth including licenses and subscription fees will come from products based on SOA Bartoer Positions EMS SOA Acids Flexibility to Business Processes Simon Hayward 16Feb05 Additional Information about EDA httDwwwcibercomservicesinteci rationindexcfmidcseisoaanalvsts Discussion SOA and business Gariner Positions 2005 SOA Adds Fiexibiiity to Business Processes Simon Hayti39aro 15Feb05 Additional Information about 50A Ely the end of2006 Forrester expects to see 62 of Global 2000 rms implementing SOA 41 ofthese rms have already deployed a service oriented architecture Forrest srs Business Technographics November 2005 North Lielrce39i PDF American and European Enterprise Software and 5mm Engine Migazme Services survey F iEilquot Tquotti39r so iing F39C Canneciion Magazine the dif culty and cost of modifying today39s rigid IT architectures dominated by big enterprise applications such as ERP can be so high that some companies would rather abandon new strategic initiatives than make CIBER Viewpoint a single change to the applications they already have in place Good news is on the horizon in the form ofservice oriented architecturesquot which promise to reduce ifnot remove the current obstacles iLri39cKirrsey Quartedy quotFlexible iT Better Strategy J Seeiy Brown and J Hagei iii httDwwwcibercomservicesinteci rationindexcfmidcseisoaanalvsts SOA III Is SOA really needed III Why is SOA adopted III If not SOA what Check this out III Translate text between two languages httDbabelfishaltavistacom III Track the current location of a package wwwfedexcomustrackino III Validate an email address httDwscdvnecomemailverifvemailvernotestemailasmx El Find info about sky resorts httpwwwskiwherecom III Address validation httDwwwserviceobiectscomDefaultasobhco1 III Currency converter httowwwwebservicexnetWSdefaultasox
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'