文档介绍：IssuesinSoftwareTestingwithModelCheckers VadimOkun NationalInstituteofStandardsandTechnology Gaithersburg,MD20899 {vokun1, }***@ ENERATINGSOFTWARETESTS Mostsoftwaredevelopersconsiderformalmethodstoohard , “light-weight” formalmethodtocheckthetruth(orfalsity)ofstatements. WeusetheSMVmodelcheckeraspartofahighlyautomated testgenerationtool,whichwehopewillmotivatepractitioners ,anizationis morelikelytoexpendtheconsiderableefforttodevelopa formalspeci?cationif,withalittleextraeffort,itcanalsoget checkerstogeneratetests. Modelcheckingisbeingappliedtotestgenerationand coverageevaluation[3],[4],[7].Inbothuses,one?rstdecides onanotionofwhatpropertiesofadesignmustbeexercised . Oneappliesthechosentestcriteriatothespeci?cationto derivetestrequirements,.,asetofindividualproperties tobetested,representedastemporallogicformulas[2].To generatetests,therequirementsmustbenegativerequirements, thatis,theyareconsideredsatis?edifthecorresponding alsobeofaformthatasinglecounterexampledemonstrates theinconsistency(exhaustiveenumerationisneededtoshow inconsistencyofanexistentialrequireme