Experience in Developing and Testing Network Proto

ExperienceinDevelopingandTestingNetworkProtocolSoftwareUsingFDTs?M.¨UmitUyaraMariuszA.Feckob;1AliY.Dualec;2PaulD.AmerdAdarshpalS.SethidaElectricalEngineeringDepartmentTheCityCollegeoftheCityUniversityofNewYork,NY,USAbAppliedResearchArea,TelcordiaTechnologies,Inc.Morristown,NewJersey,USAcEngineeringSystemsTest,IBMPoughkeepsie,NewYork,USAdComputerandInformationSciencesDepartmentUniversityofDelaware,Newark,DE,USAAbstractThispaperpresentstheresearchefforttoformallyspecify,developandtestacomplexreal-lifeprotocolformobilenetworkradios(MIL-STD188-220).Asaresult,theteamofresearchersfromtheUniversityofDelawareandtheCityUniversityoftheCityCollegeofNewYork,collaboratingwithscientistsfromCECOM(anR&DfacilityoftheU.S.Army)andtheU.S.ArmyResearchLaboratory,havehelpedadvancethestate-of-the-artinthedesign,development,andtestingofwirelesscommunicationsprotocols.EstelleisusedbothastheformalspecificationlanguageforMIL-STD188-220andthesourcetoautomaticallygenerateconformancetestsequences.Theformaltestgenerationeffortidentifiedseveraltheoreticalproblemsforwirelesscommunicationprotocols(possiblyapplicabletonetworkprotocolsingeneral):(1)thetimingconstraintproblem,(2)thecontrollabilityproblem,(3)inconsistencydetectionandeliminationproblemand(4)theconflictingtimersproblem.Basedonthecollaborativeresearchresults,twosoftwarepackageswerewrittentogenerateconformancetestsequencesforMIL-STD188-220.ThesepackageshelpedgeneratetestsforMIL-STD188-220’sDataLinkTypes1and4servicesthatwererealizablewithouttimerinterruptionswhileprovidinga200%increaseintestcoverage.ThetestcaseshavebeendeliveredandarebeingusedbyaCECOMconformancetestingfacility.Keywords:conformancetesting,Estelle,formaldescriptiontechnique,formalspecification,MIL-STD188-220,protocolspecification,testcasegeneration,PACSPreprintsubmittedtoElsevierScience1IntroductionComplexityofthewirelessprotocolsusedinMIL-STD188-220,beingdevelopedformobilecombatnetworkradios[23],necessitatedthataformalapproachbetakeninprotocolspecification,developmentandtesting.Estelle[40]waschosenastheformalspecificationlanguagetodefinetheprotocolsinMIL-STD188-220,fromwhichtheconformancetestswereautomaticallygenerated.Letusfirstprovidethefollowingdatatohelpthereaderrealizethemagnitudeofsizeandcomplexityofthewirelessprotocolsusedin188-220.TheDatalinkandNetworklayerspecificationsconsistof69and19documents,respectively,describ-ingthearchitecture,interfaces,EFSM,andstatetableofeachmodule.TheDatalinklayerspecificationisaccompaniedbythreeEstellesourcecodefiles(forDatalinkclassesA,B,andC)withapproximately1,600,8,700,and2,400linesofcode,re-spectively.TheEstellesourcecodefortheNetworklayerhas7,150linesofcode,defining34statesand370transitionsin7EFSMs(fordetails,consult[88]).AutomatictestgenerationfromEstellespecificationspresentedvarioustheoreticalproblemsdefinedasfollows:Timingconstraintproblem[79]:Duringtesting,ifactivetimerswerenottakenintoaccountwhenthetestsweregenerated,thesetimerscandisruptthetestsequences,therebyfailingcorrectimplementationsorworse,passingincorrectones.Foraccuratetesting,timersmustbeincorporatedasconstraintsintotheextendedFSM(EFSM)modelofanEstellespecification.Controllabilityproblem[32,33]:Testsequencegenerationislimitedbythecon-trollabilityofanImplementationUnderTest(IUT)[8].Testersmaynothavedirectaccesstoallinterface(s)inwhichtheIUTacceptsinputs.Typically,theinterfaceswithupperlayers,orwithtimersaredifficultorimpossibletoaccessduringrealtestingconditions.Inthiscase,someinputscannotbedirectlyap-plied;theinteractionsinvolvingsuchinterfacesmayrendersomeportionsoftheprotocoluntestable,andmayintroducenon-determinismand/orraceconditionsduringtesting.Inconsistencydetectionandeliminationproblem[25,26]:Infeasibletestsequencesmaybegeneratedunlesspossibleconflictsamongtheprotocol’svariablesusedintheactionsandtheconditionsareavoided.Conflictingtimersproblem[34]:Infeasibletestsequencesmayresultfromapro-?ThisworksupportedbytheUSARO(DAAH04-94-G-0093),andpreparedthroughcol-laborativeparticipationintheAdvancedTelecommunications/InfoDist’nResearchPro-gram(ATIRP)ConsortiumsponsoredbytheUSArmyResearchLabunderFedLabPro-gram,CooperativeAgreementDAAL01-96-2-0002.1M.FeckoperformedthisresearchwhileaPost-DocFellowattheUniv.ofDelaware.2A.DualeperformedthisresearchaspartofhisPhDworkattheCityCollegeofNewYork.2tocol’svariablesmodelingmultipletimersthatmayberunningsimultaneously.Theteamofresearchersandscientiststhatparticipatedinthisresearchanddevelop-menteffortarefromtheUniversityofDelaware(UD),theCityCollegeoftheCityUniversityofNewYork(CCNY),theArmyResearchLaboratory(ARL),USArmyCommunications-ElectronicsCommand(CECOM),andtheJointCombatNetRa-dioWorkingGroup(CNR-WG).Asaresultofthiscollaboration,thesynergisticframeworktodevelopC4I(Command,Control,Communications,Computers,andIntelligence)systemswiththehelpofformalmethodsservesasamodelforfutureU.S.DepartmentofDefensenetworkingstandardsdevelopment[27].Basedonthesolutionstothesetheoreticalproblems,twosoftwarepackages,calledefsm2fsm-rcpt,and(2)INDEEL,havebeendevelopedtoautomaticallygeneratetestcasesfrom