Model Based Testing of Large-scale Software How Can Simple Models Help to Test Complex Syst

System󰀁

VictorV.Kuliamin

InstituteforSystemProgrammingofRussianAcademyofSciences(ISPRAS),

B.Kommunisticheskaya,25,Moscow,Russia

kuliamin@ispras.ru

http://www.ispras.ru/groups/rv/rv.html

Abstract.Thearticleisconcernedwithanapproachtomodelbasedtestdevelopmentforlargesoftwaresystems.TheapproachpresentedisapartofUniTesKtestdevelopmenttechnology,whichisdevelopedonthebackgroundof10-yearexperienceofISPRASinverificationandtestdevelopmentforcomplexindustrialsoftware[1].Thearticlestatesthatthewell-knownsoftwareengineeringprinciplesunderlyingtheapproachandaimedatcopingwithcomplexitymakespossibleitsapplicationinsoftwareprojectsofreal-lifesizeandcomplexity.

1Introduction

Revolutionarychangesinsoftwareengineeringduringlastdecadeshavealreadybecomeacommonplace.Weseethatmodernmethods,technologies,andtoolsmakedevelopmentofsoftwaremorecomplexthancanbeevenimagined20yearsagoaneverydaypractice.Functionalityandcomplexityofmodernsystemsgrowsexponentially.Butthisevolutionhasonebigproblem–qualitycontroltechniqueslagbehindthedevelopmentonesandcannotprovidethesamelevelofqualityforcomplexsystemswithmanageablegrowthofeffort.

Whatcanhelpsoftwaredevelopmentcommunityinthissituation?Onepromisingcandidateismodelbasedtesting.Thisapproachhasseriousadvan-tagesincomparisonwithtraditionaltestingtechniques.

–Modelsandfurthertestscanbepreparedonthebaseofrequirementsanddesigndecisionsbeforetheotherpartsofsoftwareareready.Thus,thetotaltimeofproductioncyclecanbedecreased.

–Modelbasedtestingcanhelptofindunimplementedfeaturesandrequire-ments,whichcannotbedetectedbyimplementation-basedtesting.

–Modelbasedtestinghelpstoraisetheabstractionlevelofsystematictestingandtoevaluatequicklythecorrectnessoflargesubsystemsorsystemasawhole.Implementation-basedtestingcangetthisresultonlyafterthelong

󰀂

ThisworkispartiallysupportedbyRFBRgrant02-01-00959,bygrantofRussianScienceSupportFoundation,andbyProgram4ofMathematicsBranchofRAS.

waythroughthesmallestunitsandlargercomponentstointegrationandsystemtesting.Theanalogousresultsofad-hocfunctionaltestingaremuchlessreliableduetoitsunsystematiccharacter.

–Modelbasedtestinghasapotentialtomakemanageabletestingofextremelycomplexsystems,whichcannotbeadequatelytestedbyimplementation-basedtechniqueswithanacceptableeffort.Unfortunately,mostmodelbasedtestingcasestudiesdealwithsmallandsimplesystems.Suchasituationiscausedpartiallybycurrentorganizationalpatternsofindustrialdevelopment,butitisalsorelatedwiththebackgroundformalismsofmostpartofmodelbasedtestingtechniques.Theyarebasedusu-allyonautomatamodelsofvariouskinds(FSMs,LTSs,EFSMs,etc.).Automatamodelsofreallifesoftwarewithcomplexfunctionalityoftenhavelargenumbersofstatesandtransitionsmakingsuchmodelbasedtestingmethodsunmanage-able(thisissocalled‘stateexplosionproblem’).So,themostimportantstate-mentthatmodelbasedtestinghelpstocopewithincreasingcomplexitystillneedstobecorroborated.

Itseemsthatthemankindhasnoothertoolstocopewithcomplexitythanthewell-knownsoftwareengineeringprinciples:abstraction,modularization,andseparationofconcerns.So,thesearchforscalablemodelbasedtestingtechniquesshouldpayattentiononthefollowingtwoissues.

–Themodelsusedbyappropriatestechniquesshouldadmitsmoothintegra-tionwiththisprinciples.

–Thewell-scalablestructureofthetestsystemshouldbecomeoneofthemainconcernsofthetechnique.Thereisnowaytotestanactuallycomplexsystembothinanadequateandsimpleway.Butmaybewecanfindanorganizationalapproachthatmakesmuchmoreeasytomanagethecomplexworkweshoulddointhecase.Thus,simplemodelscanhelptotestcomplexsystemsonlyifweknowhowtoorganizethemincomplexstructuresinmanageableway.Thisarticleprovidesapossibleapproachtomanageabletestconstructionforcomplexsoftwarebasedontheprinciplesstated.TheapproachpresentedisapartofUniTesKtestdevelopmenttechnologydesignedinISPRASonthebaseon10yearexperienceintestdevelopmentforcomplexindustrialsoftware.Itusescontractspecificationsthatprovidecomponentwisedescriptionofthefunctionalityofthesystemundertestandmoreabstractautomatamodelsthatareusedtocreatetestsfordifferentaspectsanddifferentpartsofthesystem.Thenextsectionofthearticledealswithmainissuesoftheapproach.Thethirdsectionpresentstheresultsofacasestudy.Thefourthonegivesabriefoverviewofrelatedworksandcomparesthemwithourapproach.Theconclusionsummarizesthemainresultsofthearticle.

2TheApproach

TheapproachpresentedherewasdevelopedformodelbasedtestingoflargesystemsinthecontextofUniTesKtestdevelopmenttechnology.Itisusedto

2

developfunctionaltestscheckingconformancebetweenthesystemanditsmodelandconsistsonthefollowingmainsteps.

–Step1.Interfacedefinition.Wedefineclearlytheinterfaceundertestandtheabstractionlevelofthefuturetesting.Afterthisstepweshouldhavealistofoperationsandeventsinthesystemundertest,whichshouldbetestedortrackedbythetests,andanunderstandingwhatshouldbecheckedintestsandwhatshouldnot,becauseitisconsideredasimplementationspecifics.–Step2.Modeldevelopment.Afterdefinitionoftheinterfaceweshouldprovideastrictdefinitionofitspropertiesintheformofsoftwarecontracts–preconditionsandpostconditionsofoperationsandevents,dataintegrityconstraintsforallobservabledatatypes(parametersandresultsofoper-ationsandevents).Towritemeaningfulpreconditionsandpostconditionswemayneedthecorrespondinglyabstractedmodelstatealsorepresentedasdatawithsomeintegrityconstraints.Themodelstateandsoftwarecontractsprovideabehaviormodelofthesystemundertestontheabstractionlevelchosen.

–Step3.Adapterdevelopment.Thuswehavethemodelandthemod-eledsystemandwishtotesttheirconformance.Weneedfirsttoprovidesomelinksbetweentheircomponents.Usuallythistaskissolvedbymeansofadapters.InUniTesKtheyarecalledmediatorsforhistoricalreasons.Mediatorofanoperationimplementssomemodeloperationbymeansoftransformationofitscallsintocorrespondingcallsoftheoperationsofthesystemundertest.Mediatorofanevent,onthecontrary,waitsforthecor-respondingeventinthesystemundertestandtransformsittothemodelrepresentation.

–Step4.Testscenariodevelopment.Thedescriptionofthetestisrep-resentedasatestscenario.Whilethemaingoalofbehaviormodelistodescribewhatthesoftwareundertestistodo,thegoalofscenariosistoprovidedatafortestinputandtestsequencegeneration.Eachscenariohasitsspecificobjectiveusuallyrepresentedasacoverageleveltobeachievedaccordingtosomecoveragecriterion.Coveragecriteriaaredefinedintermsofthebehaviormodelandcanbeconsideredassetsofspecificsituationscalledcoveragegoals.Acoveragegoalcorrespondstoasituationwheresomepredicateonthemodelstateandparametersofthemodeloperationscalledbecomestrue.Coveragegoalcanbedefinedexplicitlybysuchapredicateorimplicitlybypointingoutthecorrespondinglocationinthecodeofop-eration’spostcondition.Inthesecondcasethecorrespondingpredicateisextractedautomatically.

Testscenariorepresentsanothermodelofthesystem’scomponentunderconsideration.Thismodelisafinitestatemachine(FSM)orinput/outputfinitestatemachine(IOFSM)havingasetofstatesSandasetoftransitionsT.Eachtransitioncorrespondstoasequenceofcallsofmodeloperations(letusdenoteallpossiblesuchcallsasCalls)andoccurrencesofmodelevents.Testscenariodescribesthegenericstatemachineinimplicitform,namely,insteadofexplicitdescriptionofallSM’sstatesandtransitions(eachhaving

3

startingstateandendstate),testscenarioconsistsofthefollowingdata(inthefollowingObsdenotesalltheobservabledataofboththebehaviormodelandthesystemundertest).

•ThedatatypeofpossibleSMstatesS.

•Thefunctionmappingtheobservabledataintoastatest:Obs→S.Onlythosestates,whichareactuallyreachedduringthetestexecution(thatis,returnedbythisfunctiononsometestingstep)areconsidered.•Thefunctionreturningadmissiblecallsofmodeloperationsinthecur-rentstateact:S×N→Calls∗,(s,i)→(c1,...cn).Thesequenceofcalls(c1,...cn)∈Calls∗shouldbeexecutedwhenthetestcomestothestatesoni-thtime.Werequirethatforeachs∈Sthereexistssomen∈Nthatact(s,n)isempty.Suchemptysequencemeansthatthetesthasalreadyperformedallthenecessaryoperationsinthisstateduringthepreviousvisitstoit.

Statesandoperationcallsinparticularscenarioaredefinedinsuchawaythatthetestobjectivestatedcanbeachievedbyperformingatransitiontouronthestatemachinedescribed.

Theapproachpresentedconsistentlyappliesthreefundamentalprinciplesofsoftwareengineering–modularization,abstraction,andseparationofconcerns,totestsystemconstruction.

–Modularization.

•Thesystemundertestisconsideredasanumberofinteractingcompo-nents,whichshouldbemodeledseparately.Thepartitioningofthesys-temintocomponentsisperformedonseverallevelsofabstractionandonthehighestoneitcanberepresentedasthesinglecomponent.Suchanapproachmakespossibletoachievehighqualitytestingofcomponentsofonelevelofabstractiononthebaseofhypothesesonreliabilityoflower-levelcomponentstestedpreviously.

Suchanapproachrequiresfromthemodelingtechniqueusedtobewellmodularizeableandusefulonlargerangeofabstractionlevels.Contractspecificationsseemtofitboththeserequirementsmorethananyothermodelingformalism.Aftertestingtheconformanceofacomponenttoitsformallyspecifiedcontractwecanrelyonthiscomponentinconstructionofhigher-levelones.

•Eachcomponentistestedseparatelyfromtheothersonthesameab-stractionlevel,butonlyaftertestingoflower-levelsubcomponents.Fortheconvenienceoftestdevelopersoperationsrathercloseconceptually,butwithoutdependenceonstatescanbecomposedinstatelesscompo-nentsandtestedtogether.Anexampleofsuchacomponentisgroupofoperationsimplementingprimitivemathematicalfunctions.•Thetestsarealsomodularized.Eachtestconsistsof

∗Atestengineimplementingparticularalgorithmoftestsequenceconstructionforgeneralscenario

∗Atestscenario,whichprovidesdatafortestsequenceconstruction

4

∗Anumberofiteratorsprovidingdatafortestinputgenerationforseparateoperationsundertest

∗Anoracleforeachoperationundertestandeacheventtrackedinthistest.Oracleisgeneratedfrombehaviormodelandcheckstheconformancebetweentheactualbehavioroftheoperationoreventanditscontract.

∗Mediatorsforeachoperationundertestandeacheventtracked.

–Abstraction.

•Functionalityofoperationsundertestisdescribedintheformofsoft-warecontractsonthedesiredabstractionlevel,whichhideimplementa-tionspecificsandmakemoreclearessentialpropertiesofthesoftwareundertest.Thismakespossibleconstructionofreusabletests,whichcanbeappliedtoanysystemequivalenttotheoriginaloneonthecho-senabstractionlevelandtootherversionsofthesystemundertestinparticular.

•Softwarecontractsareratherflexiblemodelingtechniquecapabletocap-turethepropertiesrequiredondifferentlevelsofabstraction,startingfromtheparticularalgorithmused.

Letusconsiderthecomponentimplementingthefunctionalityofab-stractmapmappingintegerstoobjects(inrealityitcanhavemorespecificform,likeindexedrecordsindatabaseorpoolofobjectsusedbyWeb-server).Themainoperationsofsuchamapareadditionofakey-objectpairboolAdd(intkey,objectvalue)(returnstrueiffthepairisadded,falseiffthekeyisalreadyusedinthemap),checkwhetherakeyvalueisalreadyusedboolContainsKey(intkey),searchofanobjectbyitskeyobjectGet(intkey)(canbecalledonlyforusedkeys),andremovalofakeyalongwiththecorrespondingobjectvoidRemove(intkey)(canbecalledonlyforusedkeys).Fig.1inAppendixdemonstratesthedetailedcontractofthiscomponentintheextensionofC#languageusedbyoneofUniTesKtools,Ch@se.

Wecaneitheraddmoredetailstothatspecificationbyrefiningthenatureofobjectsstoredinmap,orskipsomedetails,forexample,donotcheckframeconditionsstatingthatthepartsofstatenottouchedbytheoperationarepreserved.Orwecanabstractfromstoredobjectsatallreducingamapdescribedtothesetofitskeys.

•Testscenariosprovidemoreabstractviewonthecorrespondingaspectofthesystemfunctionality.Namely,theyabstractfromallthedetailsthatarenotneededtoconstructatestsequenceachievingthecoveragedesired.

Testscenariocanabstractthecomponentstateindifferentwaysaccord-ingtoitsgoals.Forexample,Fig.2inAppendixdemonstratesthetestscenariofortestingthemapdescribedabove.Itdefinesthestatemachinewithstatescorrespondingtodifferentnumbersofkey-valuepairsinthemapundertest.ThescenarioshownonFig.3definesthestateasthesetofintegersusedaskeys,soitprovidesmuchmoredetailedtestingof

5

thecomponent.NotethatweneedonlytooverrideStatepropertyoftestscenariotomakethisrefinement.

–SeparationofConcerns.Separationofconcernsprincipleisimplementedbothbetweenthecomponentsthatuserhastodeveloptoconstructfullyfunctionaltestandbetweenthecomponentsoftheresultingtests.

•Contractspecificationsprovidestrictdescriptionoffunctionalrequire-mentstocorrespondingoperationsandeventsofthesystemundertest.Theygivemeanstochecktheconformancebetweenthisrequirementsandthesystem’sactualbehavior.

•Coveragecriteriaprovidedescriptionoftestadequacycriteria,whichareusedtomeasuretheadequacyofresultingtestsandtoaimtestscenariosatachievinghighlevelsoftestingquality.

•Mediatorsprovidebindingbetweenmodelandthesystemundertestduringtestexecution.Mediatortransformscallsofmodeloperationsintocorrespondingcallsofimplementationoperationsandtransformstheresultofimplementationcalloreventonmodellevel.

•Iteratorsprovidedataforgenerationofoperations’parametersvaluesduringtestexecution.

•Testscenario’sconcernistoprovidedatafortestsequencegenerationduringtestexecution.

•Testengine’sconcernistoconstructaneededpathontheFSMimplicitlydescribedbythetestscenariousedintestconstruction.Tosolvethistaskitcanuseonlythedataonthealreadyexecutedtransitionsandvisitedstates,soUniTesKtestenginesarebasedonalgorithmsforunknowngraphexploration.Thiscombinationoffundamentalsoftwareengineeringprinciplesandspecialattentiononmodularizationaspectsmaketheapproachusefulformanageabletestdevelopmentforlarge-scalesoftware.ThisstatementcanbeconfirmedbysuccessfuluseofUniTesKintestingoflargeandcomplexsystems.

3TheCaseStudy

TheoriginofUniTesKtechnologyisrelatedwithtelecommunicationsoftwareverificationprojectconductedbyISPRASforNortelNetworksin1994-1996[2].Theprojectgoalwastodeveloparegressiontestsuiteforkerneloftheoperatingsystemoftelecommunicationswitch.Thetotalsizeofthesystemundertestwasabout250Klinesofcode.Theinterfaceundertestconsistedofmorethan500operationsandincludedsuchfunctionalityasarithmeticoperationswithbasicandextendednumbertypes,timedataconversion,messagingmanagement,pro-cessmanagement,synchronizationmanagement,processresourcesmanagement,andsoon.

Theresultingtestsuitepartitionedtheinterfaceundertestinto44compo-nents(inthiscaseitwasgroupsofoperationsdependentfromeachother),fromwhich29componentswerestatefull.Totalsizeofthespecificationwrittenis

6

about60Klinesofcode.Totalsizeofcodeofmediatorsdevelopedisabout50Klines.372testscenariosweredeveloped,304forstate-independentoper-ationsand68forstatefullcomponents.Theirtotalsizeisabout80Klinesofcode.Thetotaleffortoftheprojectwasabout10man-year(thetotaleffortofdevelopmentofthesystemundertestisabouttentimesmore).

ThetestsuitedevelopedwasusedforregressiontestingoftheOSkerneltill2000.Itwasusefulnotonlytheregressiontestsuite,sincemorethantwohundrederrorswerefoundinthefieldversionoftheOSwithitshelpandseveraldozensofthemwereshowstoppers–theyrequiredcoldrestartofthesystemtorestoreitintheoperatingstate.

4RelatedWorks

Authorknowsonlyseveralworksconcernedwithmodelbasedtestingoflargesoftware.Thebibliographyanalysisshowsthatthemostpartofmodelbasedtestingsocietytendstoworkwithtoyandsmall-sizeexamples.Thisisreallyunfortunateforpropagationofmodelbasedapproachtotestingintheindus-try,sincemostsignificantproblemsoftraditionaltestingtechniquesarerelatedwithlarge-scaleandcomplexsystems.OnecauseofsuchasituationisV-modelstereotypeforsoftwaredevelopment,whichseemstoprescribetestdevelopmentintheinverseordertothemaindevelopmentactivity–unittestsfirst,thentestsforlargerunitsandcomponents,thenintegrationtests,andonlythemsystemtests.Theauthorthinksthatcomplexityandgiganticsizeofmodernsystemsurgentlyrequiresnewtestdevelopmenttechniquesthatcanbestartedonhighorintermediatedesignlevel.

Thefirstgroupofworksrelatedwiththelarge-scalemodelbasedtestingisconcernedwitharchitecture-basedtesting.TheworksofA.Bertolino,P.Inver-ardiandH.Muccini[3–6]andrelatedarticleofD.RichardsonandA.Wolf[7]useinformalarchitecture-leveldescriptionofsoftwareundertesttoconstructLTSmodelsfordifferentaspectsofthesoftwareandthenderivetestsfromthem.Theirapproachmostlyfocusedonintegrationtestingandcheckingtheinterac-tionoflargecomponentsofthesystemundertest.UniTesKapproachpresentedinthisarticlecanbeusedbothforunittestingandforintegrationtesting.Onemoredifferenceofthetwoapproachesliesinthemodelsused–UniTesKusescontractspecificationsforlow-leveldescriptionsandFSMs(alongwithIOFSMs)forhigher-levelmodeling,andtheauthorsciteduseLTSsforbothdetailedandabstracteddescriptions.

TheothergroupofworksontestingcomplexsoftwaresystemsknowntotheauthorisrelatedwithCˆotedeResysteproject[8–11].Theparticipantsofthisprojectdevelopedthetechniquesandtools(TorXandTGV)capabletocon-structmodelbasedtestsfromtheLTSmodelsanduserdefinedtestpurposes.Thetoolsweresuccessfullyusedintestingreal-lifesoftwareapplications.ThemostprominentisusingTorXintestingtheOosterscheldeStormSurgeBar-riercontrolsoftware,whichcodesizeisabout80Klines.TheapproachusedinCˆotedeResytetoolsisclosetotheonepresentedinthispaper.Maindifferences

7

arerelatedwithuseofcontractspecificationsandcoveragecriteriabasedontheminUniTesKanduseofonlyLTSmodelsinCˆotedeResyste.TheworksofJ.Tretmansaremostlyfocusonformaldefinitionoftestedconformancerela-tionbetweenmodelandimplementation.TherelationusedinUniTesKismorecomplex,sinceitincludescontractspecifications.Somedetailsonthistopiccanbefoundin[12].

5Conclusion

TheUniTesKapproachformodelbasedtestingwasdesignedonthebaseofawell-knownsetofprinciplesthatareaimedatcopingwithcomplexity.Thishelpstouseitforlarge-scalesoftwaretestingwitheffortcomparablewithtraditionaltestdevelopment,butwithmuchhigherqualityofresultingsoftware.Italsoincludestechniquesformodelingconcurrencyandtimingpropertiesoftestedsoftwareinanenvironmentfamiliarforindustrialdevelopers[13].InadditionUniTesktoolsarebasedonextensionsofwidelyusedprogramminglanguages.Thatfactfacilitatesintroductionoftheapproachintoindustrialprocesses.

Theresultsofcasestudies[14]ofusingtheapproachtotestindustrialsoft-wareofvariousdomainsshowitsapplicabilityforalargevarietyofcontexts.Nowitscasestudydatabaseincludes,besideskernelverificationprojectpre-sentedabove,testdevelopmentforseveraldifferentIPv6implementations,bank-ingclientmanagementsoftwaresystembasedonJ2EEandWebtechnologies,messagingsystems,devicedrivers,etc.

Ofcourse,studiesontheapproachapplicabilitytovariousprojecttypesandcomparativeevaluationofeffortneededtodeveloptestsusingdifferenttech-niquesshouldbecontinued.Butthedatawealreadyhavedemonstratethatmodelbasedtestingcanprovideactualhelpindevelopmentofmodernsoftwaresystemshavingcomplexfunctionalityandintractablebymeansoftraditionaltestingmethods.

References

1.http://www.ispras.ru/groups/rv/rv.html

2.I.Bourdonov,A.Kossatchev,A.Petrenko,andD.Galter.KVEST:AutomatedGenerationofTestSuitesfromFormalSpecifications.FM’99:FormalMethods.LNCS1708,Springer-Verlag,1999,pp.608–621.

3.A.Bertolino,P.Inverardi.Architecture-basedSoftwareTesting.InjointACMpro-ceedingsofthe2-ndInternationalSoftwareArchitectureworkshop(ISAW-2)andInternationalWorkshoponMultiplePerspectivesinSoftwareDevelopment(View-points’96)onSIGSOFT’96workshops,pp.62–64,October1996.

4.A.Bertolino,P.Inverardi,H.Muccini,andA.Rosetti.AnApproachtoIntegrationTestingBasedonArchitecturalDescriptions.InProc.ThirdIEEEInternationalConferenceonEngineeringofComplexComputerSystems(ICECCS97),pp.77–84,Como,Italy,September1997.

5.A.Bertolino,F.Corradini,P.Inverardi,andH.Muccini.DerivingTestPlansfromArchitecturalDescriptions.InProc.22-ndInternationalConferenceonSoftwareEngineering(ICSE’2000),pp.220–229,Limerick,Ireland,June2000.

8

6.H.Muccini,A.Bertolino,andP.Inverardi.UsingSoftwareArchitectureforCodeTesting.IEEETransactionsonSoftwareEngineering,Vol.30,No.3,pp.160–171,March2004.

7.D.J.Richardson,A.L.Wolf.Softwaretestingatthearchitecturallevel.Injointproceedingsofthe2-ndInternationalSoftwareArchitectureworkshop(ISAW-2)andInternationalWorkshoponMultiplePerspectivesinSoftwareDevelopment(Viewpoints’96)onSIGSOFT’96workshops,pp.68–71,October1996.

8.J.Tretmans.Testgenerationwithinputs,outputsandrepetitivequiescence.Soft-ware–ConceptsandTools,17(3):103–120,1996.Also:TechnicalReportNo.96-26,CentreforTelematicsandInformationTechnology,UniversityofTwente,TheNetherlands.

9.J.Tretmans.TestingConcurrentSystems:AFormalApproach.InJ.C.M.BaetenandS.Mauw,editors,CONCUR’99–10-thInt.ConferenceonConcurrencyThe-ory,volume1664ofLectureNotesinComputerScience,pp.46–65.Springer-Verlag,1999.

10.A.Belinfante.TimedTestingwithTorX:TheOosterscheldeStormSurgeBarrier.

InM.Gijsen,editor,Handout8eNederlandseTestdag,Rotterdam,TheNether-lands,November,2002,CMG.

11.J.Tretmans,E.Brinksma.TorX:AutomatedModelBasedTesting.Cˆotede

Resyste.InProc.ofECMDSE’2003,Nuremberg,Germany,December2003.

12.V.Kuliamin.Multi-paradigmModelsasSourceforAutomatedTestConstruction,

InProc.ofModelBasedTestingworkshoponETAPS’2004,Barcelona,Spain,March2004.

13.V.Kuliamin,A.Petrenko,N.Pakoulin,I.Bourdonov,andA.Kossatchev.Integra-tionofFunctionalandTimedTestingofReal-timeandConcurrentSystems.Proc.ofPSI2003,LNCS2890,pp.450–461,Springer-Verlag,2003.14.http://www.unitesk.com

6Appendix

Appendixcontainstheexampleofspecificationsofacomponentimplementingmapmappingintegerstoobjects.SpecificationiswrittenintheextensionofC#usedbyoneofUniTesKtools.Twoexamplesoftestscenariosforthesamecomponentarealsopresentedhere.

9

namespaceChase.Examples{

specificationpublicclassIntToObjectMapSpecification{publicHashtableitems=newHashtable();

invariantI(\"Keysareintegers\"){foreach(objectoinitems.Keys)if(!(oisint))returnfalse;returntrue;}

specificationpublicboolAdd(intkey,objectvalue)readskey,valueupdatesitems{

post{

if(!items.Keys.Contains(key)){

branchUnusedKey(\"Thekeyisnotused\");Hashtableold=(Hastable)(items.Clone());old.Remove(key);

return$this.Result==true&&old.Equals(preitems.Clone());}else{

branchUsedKey(\"Thekeyisused\");

return$this.Result==false&&items.Equals(preitems.Clone());}}}

specificationpublicboolContainsKey(intkey)readskey,items{

post{

branchSingle(\"Singlebranch\");return$this.Result==items.Keys.Contains(key)

&&items.Equals(preitems.Clone());

}}

specificationpublicobjectGet(intkey)readskey,itemsupdatesitems{

pre{returnitems.Keys.Contains(key);}post{

branchSingle(\"Singlebranch\");return$this.Result==items[key]

&&items.Equals(preitems.Clone());

}}

specificationpublicvoidRemove(intkey)readskey

updatesitems{

pre{returnitems.Keys.Contains(key);}post{

branchSingle(\"Singlebranch\");

Hashtableold=(Hastable)(preitems.Clone());old.Remove(key);

returnold.Equals(items);}}}}

Fig.1.ExampleofspecificationsinC#extension

10

namespaceChase.Examples{

scenariopublicclassMapTestScenario{publicstaticvoidMain(){Tracer.Init();

MapTestScenariotest=newMapTestScenario(13);test.Run();

Tracer.Finish();}

IntToObjectMapSpecificationtarget=newIntToObjectMapSpecification();intmaxNumber=10;

protectedvirtualvoidconfigureMediators(){

target=mediatorIntToObjectMapMediator(newIntToObjectMap());target.AttachOracle();}

publicMapTestScenario(intmaxNumber){

Engine=newChase.Engines.DFSWithSCEngine();this.maxNumber=maxNumber;configureMediators();}

publicoverrideChase.Lang.ModelObjectState{

get{returnnewChase.States.IntState(target.items.Count);}}

scenarioAdd(){

if(target.items.Countiterate(inti=0;iscenarioContains(){

iterate(inti=0;iscenarioGet(){

iterate(inti=0;iscenarioRemove(){

iterate(inti=0;iif(target$Remove.pre(i))target.Remove(i);returntrue;}}}

Fig.2.ExampleoftestscenarioinC#extension

11

namespaceChase.Examples{

scenariopublicclassDetailedMapTestScenario:MapTestScenario{

publicstaticvoidMain(){Tracer.Init();

MapTestScenariotest=newDetailedMapTestScenario(5);test.Run();

Tracer.Finish();}

publicDetailedMapTestScenario(intmaxNumber){base(maxNumber);}

publicoverrideChase.Lang.ModelObjectState{get{

IntSetStatestate=newIntSetState();foreach(objectointarget.items.Keys)state.Add(oasint);returnstate;}}}}

Fig.3.ExampleofmoredetailedtestscenarioinC#extension

12