文档介绍：SoftwareModelChecking forEmbeddedSystemsPIs:MatthewDwyer1,JohnHatcliff1,eAvrunin2Post-docs:StevenSeigel2,RaduIosif1Students:Robby1,RobyJoehanes1,YuChen1KansasStateUniversity1UniversityofMassachusetts2TheDreamProgramRequirementCheckervoidadd(Objecto){buffer[head]=o;head=(head+1)%size;}Objecttake(){…tail=(tail+1)%size;returnbuffer[tail];}Property1:…Property2:……OKErrortraceorModelCheckingFinite-statemodelTemporallogicformulaModelChecker(FW)OKErrortraceorLine5:…Line12:…Line15:…Line21:…Line25:…Line27:……Line41:…Line47:…WhyuseModelChecking?Incontrasttotesting,pletecoveragebyexhaustivelyexploringallpathsinsystem,It’essinhardwareandprotocoldesignAutomaticallycheck,.,invariants,safety&livenesspropertiesabsenceofdead-lockandlive-plexeventsequencingproperties,“Betweenthekeybeinginsertedandthekeybeingremoved,theignitioncanbeactivatedatmosttwice.”Thissuggeststhatmodel--checkingsoftwaredifficult?ModelconstructionOKErrortraceorFinite-statemodelTemporallogicformulaModelChecker(FW)StateexplosionProblemsusingexistingcheckers:PropertyspecificationOutputinterpretationLine5:…Line12:…Line15:…Line21:…ModelConstructionProblemSemanticgap:ModelDescriptionModelCheckerProgramvoidadd(Objecto){buffer[head]=o;head=(head+1)%size;}Objecttake(){…tail=(tail+1)%size;returnbuffer[tail];}GapProgrammingLanguagesModelDescriptionLanguagesmethods,inheritance,reation,exceptions,“Betweenthekeybeinginsertedandthekeybeingremoved,theignitioncanbeactivatedatmosttwice.”[]((keyIn/\<>keyRem)->((!activate/\!keyRem)U(keyRem\/((activate/\!keyRem)U(keyRem\/((!activate/\!keyRem)U(keyRem\/((activate/\!keyRem)U(keyRem\/(!activateUkeyRem))))))))))…isrenderedinLTLas...StateExplosionProblemMoore’slawandalgorithmadvancescanhelpHolzmann:7days(1980)==>7seconds(2000)ExplosivegrowthofsoftwarelimitsscalabilityBitx1,…,xN2^ponents