ltl和CTL讲义.ppt

LinearTemporalLogic LinearTemporalLogic LTL LTLNotes InventedbyPrior 1960 s andfirstusetoreasonaboutconcurrentsystemsbyA Pnueli Z Manna etc LTLmodel checkersareusuallyexplicit statecheckersduetoconnectionbetweenLTLandautomatatheoryMostpopularLTL basedcheckerisSpin G Holzman ComputationalTreeLogic CTL ComputationalTreeLogic CTL ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ComputationTreeLogic ExampleCTLSpecifications Foranystate arequest forsomeresource willeventuallybeacknowledged AG requested AFacknowledged Fromanystate itispossibletogettoarestartstate AG EFrestart Anupwardstravellingelevatoratthesecondfloordoesnotchangesitsdirectionwhenithaspassengerswaitingtogotothefifthfloor AG floor 2 direction up button5pressed A direction upUfloor 5 CTLNotes InventedbyE ClarkeandE A Emerson early1980 s SpecificationlanguageforSymbolicModelVerifier SMV model checkerSMVisasymbolicmodel checkerinsteadofanexplicit statemodel checkerSymbolicmodel checkingusesBinaryDecisionDiagrams BDDs torepresentbooleanfunctions bothtransitionsystemandspecification ComparingLTLandCTL CTLisnotstrictlymoreexpressionthanLTL andviceversa CTL inventedbyEmersonandHalpernin1986tounifyCTLandLTLWebelievethatalmostallpropertiesthatonewantstoexpressaboutsoftwarelieinintersectionofLTLandCTL MotivationforSpecificationPatterns TemporalpropertiesarenotalwayseasytowriteClearlymanyspecificationscanbecapturedinbothCTLandLTL LTL P Q CTL AG P AFQ CapuretheexperiencebaseofexpertdesignersTransferthatexperiencebetweenpractictioners Weusespecificationpatternsto PatternHierarchy PropertyPatterns Occurrence Order Absence Universality Existence BoundedExistence Precedence Response ChainPrecedence ChainResponse OccurrencePatterns Absence Agivenstate eventdoesnotoccurwithinascopeExistence Agivenstate eventmustoccurwithinascopeBoundedExistence Agivenstate eventmustoccurktimeswithinascopevariants atleastktimesinscope atmostktimesinscopeUniversality Agivenstate eventmustoccurthroughoutascope OrderPatterns Precedence Astate eventPmustalwaysbeprecededbyastate eventQwithinascopeResponse Astate eventPmustalwaysbefollowedastate eventQwithinascopeChainPrecedence Asequenceofstate eventsP1 Pnmustalwaysbeprecededbyasequenceofstates eventsQ1 QmwithinascopeChainResponse Asequenceofstate eventsP1 Pnmustalwaysbefollowedbyasequenceofstates eventsQ1 Qmwithinascope PatternScopes Global BeforeQ AfterQ BetweenQandR AfterQandR Statesequence Q R Q Q R Q TheResponsePattern Todescribecause effectrelationshipsbetweenapairofevents states Anoccurrenceofthefirst thecause mustbefollowedbyanoccurrenceofthesecond theeffect AlsoknownasFollowsandLeads to Intent Mappings Inthesemappings PisthecauseandSistheeffect P S R P RU S R UR Q P S Q R R P RU S R UR Q R P RU S R WR Globally BeforeR AfterQ BetweenQandR AfterQuntilR LTL TheResponsePattern continued Mappings Inthesemappings PisthecauseandSistheeffect AG P AF S A P A RU S R AG R WR A QW Q AG P AF S AG Q R A P A RU S R AG R WR AG Q R A P A RU S R WR Globally BeforeR AfterQ BetweenQandR AfterQuntilR CTL ExamplesandKnownUses Responsepropertiesoccurquitecommonlyinspecificationsofconcurrentsystems Perhapsthemostcommonexampleisindescribingarequirementthataresourcemustbegrantedafteritisrequested Relationships NotethataResponsepropertyislikeaconverseofaPrecedenceproperty Precedencesaysthatsomecauseprecedeseacheffect and SpecifyPatternsinBandera TheBanderaPatternLibraryispopulatedbywritingpatternmacros pattern name Response scope Globally parameters P S format P leadsto S globally ltl P S ctl AG P AF S Evaluation 555TLspecscollectedfromatleast35differentsources511 92 matchedoneofthepatternsOfthematches Response 245 48 Universality 119 23 Absence 85 17 Questions DopatternsfacilitatethelearningofspecificationformalismslikeCTLandLTL Dopatternsallowspecificationstobewrittenmorequickly Arethespecificationsgeneratedfrompatternsmorelikelytobecorrect Doestheuseofthepattern