Using Model Checking to Generate Tests from Requir

UsingModelCheckingtoGenerateTestsfromRequirementsSpecifications*AngeloGargantinilandConstanceHeitmeyer2’PolitecnicodiMilano,Milano,[e-mail]2Code5546,NavalResearchLaboratory,[e-mail],manyformalmethods,suchastheSCR(SoftwareCostReduction)requirementsmethod,havebeenproposedforimprovingthequalityofsoftwarespecifications.Althoughimprovedspecificationsarevaluable,theultimateobjectiveofsoftwaredevelopmentistoproducesoftwarethatsatisfiesitsrequirements.Toevaluatethecorrectnessofasoftwareimplementation,onecanapplyblack-boxtestingtodeterminewhethertheimplementation,givenasequenceofsysteminputs,producesthecorrectsystemoutputs.Thispaperdescribesaspecification-basedmethodforconstructingasuiteoftestsequences,whereatestsequenceisasequenceofinputsandoutputsfortestingasoftwareimplementation.ThetestsequencesarederivedfromatabularSCRrequirementsspec-ificationcontainingdiversedatatypes,i.e.,integer,boolean,andenu-meratedtypes.PromthefunctionsdefinedintheSCRspecification,themethodformsacollectionofpredicatescalledbranches,which“cover”allpossiblesoftwarebehaviorsdescribedbythespecification.Basedonthesepredicates,themethodthenderivesasuiteoftestsequencesbyusingamodelchecker’sabilitytoconstructcounterexamples.Thepaperpresentstheresultsofapplyingourmethodtofourspecifications,includ-ingasizablecomponentofacontractorspecificationofarealsystem.1IntroductionDuringthelastdecade,numerousformalmethodshavebeenproposedtoim-provesoftwarequalityandtodecreasethecostofsoftwaredevelopment.Oneofthesemethods,theSCR(SoftwareCostReduction)method,isbasedonauser-friendlytabularnotationandoffersseveralautomatedtechniquesforde-tectingerrorsinsoftwarerequirementsspecifications,includinganautomatedconsistencycheckertodetectmissingcasesandotherapplication-independenterrors[14];asimulatortosymbolicallyexecutethespecificationtoensurethatitcapturestheusers’intent[13];andamodelcheckertodetectviolationsofcriticalapplicationproperties[3,12].Recently,groupsatNASAandRockwellAviationaswellasourgroupatNRLhaveusedtheSCRtechniquestodetectseriouserrorsinrequirementsspecificationsofreal-worldsystems[7,21,12].Byexposingdefectsintherequirementsspecification,suchtechniqueshelptheuserimprovethespecification’squality.Thisimprovedspecificationprovidesasolidfoundationforthelaterphasesofthesoftwaredevelopmentprocess.Whilehigh-qualityrequirementsspecificationsareclearlyvaluable,theulti-mateobjectiveofthesoftwaredevelopmentprocessistoproducehigh-qualitysoftware,i.e.,softwarethatsatisfiesitsrequirements.Toweedoutsoftwareerrors*ThisresearchisfundedbytheOfficeofNavalResearchandSPAWAR.147andtohelpconvincecustomersthatthesoftwareperformanceisacceptable,thesoftwareneedstobetested.Anenormousproblem,however,isthatsoftwaretest-ing,especiallyofsafety-criticalsystems,isextremelycostlyandtime-consuming.Ithasbeenestimatedthatcurrenttestingmethodsconsumebetween40%and70%ofthesoftwaredevelopmenteffort[2].Onebenefitofaformalmethodisthatthehigh-qualityspecificationitpro-ducescanplayavaluableroleinsoftwaretesting.Forexample,thespecificationmaybeusedtoautomaticallyconstructasuiteoftestsequences.Thesetestsequencescanthenbeusedtoautomaticallychecktheimplementationsoftwareforerrors.Byeliminatingmuchofthehumaneffortneededtobuildandtoapplythetestsequences,suchanapproachshouldreduceboththeenormouscostandthesignificanttimeandhumaneffortassociatedwithcurrenttestingmethods.ThispaperdescribesanoriginalmethodforgeneratingtestsequencesfromanoperationalSCRrequirementsspecificationcontainingmixedvariabletypes,i.e.,integers,booleans,andenumeratedtypes.Inourapproach,eachtestse-quenceisasequenceofsysteminputsandtheirassociatedoutputs[19].Therequirementsspecificationisusedbothtogenerateavalidsequenceofinputsandasanoracle[17]thatdeterminesthesetofoutputsassociatedwitheachinput,Toobtainavalidsequenceofinputs,theinputsequenceisconstrainedtosatisfytheinputmodel(i.e.,assumptionsabouttheinputs)thatispartoftherequirementsspecification.Ourmethodforgeneratingtestsequences“cov-ers”thesetofallpossibleinputsequencesbyorganizingthemintoequivalenceclassesandgeneratingoneormoretestsequencesforeachequivalenceclass.Section2reviewstheSCRmethod,andSection3describestheobjectivesofaneffectivesuiteoftestsequences.Aftershowinghowtestsequencescanbederivedfromsystemproperties,Section4presentsouroriginalmethodforgeneratingtestsequencesfromoperationalrequirementsspecificationsandthebranchcoveragecriterionthatthemethodapplies.Section5describesatoolwedevelopedthatuseseitheroftwomodelcheckerstoautomaticallygeneratetestsequences;italsopresentstheresultsofapplyingthetooltofourspecifications.Section6reviewsrelatedwork,andSection7presentsasummaryandplansforfuturework.2Background:TheSCRRequirementsMethodTheSCRmethodwasformulatedin1978tospecifytherequirementsoftheOp-erationalFlightProgram(OFP)oftheU.S.Navy’sA-7aircraft[15].Sincethen,manyindustrialorganizations,includingBellLaboratories,Grumman,OntarioHydro,andLockheedhaveusedSCRtospecifytherequirementsofpracticalsystems.The