Abstract RV’02 Preliminary Version Dynamic Event Generation for Runtime Checking using the

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

RV’02PreliminaryVersion

DynamicEventGenerationforRuntimeCheckingusingtheJDI1MarkBr¨orkens2

OFFIS,R&DDivisionEmbeddedSystems

Escherweg2,D–26121Oldenburg,Germany

MichaelM¨oller3

UniversityofOldenburg,DepartmentofComputerScience

Postbox2503,D–26111Oldenburg,Germany

Abstract

Approachestoruntimecheckinghavetotracktheexecutionofasoftwaresystemandthereforehavetodealwithgeneratingandprocessingexecutionevents.Oftenthesetechniquesareappliedatthecodelevel–eitherbyinsertingnewsourcecodepriortothecompilationorbymodifyingthetargetcode,e.g.Javabytecode,beforerunningtheprogram.

Thejassda[4,3]frameworkandtoolenableruntimecheckingofJavaprogramsagainstaCSP-likespeci cation.ForgeneratingeventsitusestheJavaDebugInter-face(JDI)andthusnomodi cationstothecodearenecessary.Anotheradvantageisthateventsaregeneratedondemand,i.e.dynamicallyatruntimeitisdeterminedwhicheventstogenerateforthecurrentdebugrunwithoutmodifyingtheprogramitself.Thispapershowshowthiseventgenerationisdonebythejassdaframework.1Introduction

Softwaresystemshavegrownsubstantiallysincetheinventionofmicrocom-puters.Thistrendcannotonlybeseeninthesizeofprograms,butalsoinapplicationareas.ThegrowthoftheInternetwithmoreandmoredynamicweb-pagesprovidingnewservicesforend-usersisanothercategoryofthiscomplexity.Today’ssoftwaresystemsaredistributed,workinparallelandhavetocommunicate.

1ThisworkwaspartiallyfundedbytheGermanResearchCouncil(DFG)undergrantOL98/3-1.

2Email:Mark.Broerkens@offis.de

3Email:Michael.Moeller@informatik.uni-oldenburg.de

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

Inallthesesoftwaresystemscorrectnessbecomesmoreimportantbutishardertoproveduetothegrowingcomplexity.TraditionalmethodstoprovethiscorrectnessareModelchecking[5]andProgramVeri cation[8,1].Thedevelopmentofprogramveri cationtechniquesforobject-orientedlanguages(anditssupportbytheoremprovers)isatopicofcurrentresearch(seeforinstance[9,10,18])andhavebeensuccessfullyappliedindomainspeci careasofsoftwaredevelopment.However,thesetechniquesareoftenonlyviablewithspeci cknowledgeofunderlyingtheoremproversandarethereforerestrictedtoexperts.

Runtimecheckingisalightweightformaltechniquethatwillundoubtedlynotexceedthestrengthoftheaboveheavyweighttechniques.Inthiscaseonlythecurrentrunoftheprogramischeckedagainstthespeci cation,butitiseasiertoapplyto(evenlarge)systemsandtobeusedbynon-experts.

FortheJavaprogramminglanguagemanyruntimecheckingapproachesconcentrateontheDesignbyContractconceptasproposedbyBertrandMeyerforthelanguageEi el[16].Thenamereferstoacontractwhichismadebetweentheclientandthesupplierofacomponent.Thecontractstatestheobligationsoftheclientbeforeusingamethodandtheconstraintsprovidedbythesupplierafteruseoftheservice.Thesytaxoftheseconditions,calledassertions,isusuallyclosetotheprogramminglanguage.ToolsthatprovidethisforJavaaree.g.jContractor[11],iContract[14]ortheruntime-checkerofJML[15].TheJass4tool[2]inadditionprovidesTraceAssertionsthatallowtostateconditionsdescribingtheorderofevents,i.e.methodentryandexitpoints.

IntheTrace-Checkerofjassda5theseTraceAssertionsareextendedtosupportJavaprogramsinamoregeneralway.TheeventemittingmechanismofJasswasnotsatisfying,sincetheeventemittingcodeforeverypossiblyinterestingeventhadtobeinserted.Asconsequencealotmoreeventsthanneededweregeneratedandeventsforclasseswithoutsourcecodecouldnotbegenerated.Dynamic“onthe y”generationofeventsisimportanttoreducethehugeamountofpossibleeventslikeinMorphine[6].Buttomodifythesystem-under-test(SUT)aslessaspossible,jassdausestheJavaDebugInterface(JDI)toletthevirtualmachinegeneratetheseevents.Asapositiveside-e ectitisalsopossibletomonitordistributedsystemsofcommunicatingJavaprograms,becauseanumberofJavavirtualmachinesmaybeconnected.

ThenextsectionwilldescribethearchitectureofthejassdaframeworktoexplaintheuseoftheJDI.ThefollowingsectionsdescribetheJDIandtheeventmodelusedinjassda.Furtherabenchmark,aconlusionandanoverviewofrelatedworkisgiven.

4

5JavawithassertionsJassDebuggerArchitecture

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

2ThejassdaFramework–Motivation

ThejassdatoolallowstheruntimecheckingofasystemofJavaprogramsagainstaCSP-likespeci cation.Inthisspeci cationlanguageeventshavetobeconsumedandithastobedecidedwhethertheyareconformingwiththespeci cation.Togetthoseeventsfromthesystem-under-test(SUT),i.e.asystemofJavaprograms,ageneraleventextractionanddispatchingfacilitywasdeveloped,thejassdaframework.

Thisframeworkmightalsobeusedforotherpurposes,e.g.justloggingevents6,ortostimulateaprogramfortestpurposes.

Thearchitectureofthisframeworkisshownin gure1.Atthelowestlevelthedebuggeesareshown,whichtogetherformthesystem-under-test.ThesedebuggeesareconnectedtotheBrokerwhichisthecentralcomponentofthejassdaframework.The“Registry”database,anoptionalgraphicaluserinterfaceandtheBrokerbuildthejassdacore.jassdamodulesareconnectedtothiscorerequestingandconsumingevents.

Fig.1.Architectureofjassda

Theconnectionbetweenthedebuggeesandthejassdacoretransportstheeventsthatwewanttoobserve7.ThisconnectionisestablishedbyusingtheJavaPlatformDebuggerArchitecture(JPDA)asdescribedinthenextsection.

3GeneratingExecutionEvents

Oneoftheaimsofthedesign,whendevelopingthejassdatool,wastoachieveamethodformonitoringJavaprogramsreducedtoaminimumofmodi cations6

7Thisapplicationoftheframeworkisimplementedbythe“Logger-Module”Additionallyitwillalsosendbackcontrolinformation

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

totheprogramitself.Toachievethis,theJavaDebugInterface(JDI)

[19]isused.

3.1TheJavaDebugInterface(JDI)

JDIJava

Debug

Interface

Java

Debug

Wire

Protocol

Java

Virtual

Machine

Debug

InterfaceJDWPJVMDIFig.2.JavaPlatformDebuggerArchitecture

CurrentIntegratedDevelopmentEnvironmentsforJavalikeSunForteforJava,BorlandJBuilderorIntelliJIDEAcontainadebugger,basedontheJavaPlatformDebuggerArchitecture(JPDA)forcommunicatingwiththesystemthatistobedebugged.TheJPDAconsistsoftwoprogramminginterfaces,i.e.theJavaVirtualMachineDebugInterface(JVMDI)andtheJavaDebugInterface(JDI),andoneprotocol,i.e.theJavaDebugWireProtocol(JDWP),asshownin gure2.TheJVMDIisalow-levelnativeinterfacethatde nestheserviceswhichaJavavirtualmachinemustprovidefordebugging.Thesecondinterface,theJDI,providesahigh-levelJavaprogramminglanguageinterface.TheformatofinformationandrequeststransferredbetweenthedebuggeesandthedebuggerFront-Endisde nedbytheJDWP.

Inadditiontowellknownfunctionslikesettingbreakpointsandwatchingvariables,theJDIprovidesanextendedfacilityformonitoringandmanipu-latingtheexecutionofaJavaprogram.

Duringruntimethedebuggeescanbecon guredtogenerateeventsincaseofseveralsituations,e.g.amethodhasstartedorterminated,anexceptionhasoccurred,abreakpointisreached,aclassisloaded/unloaded,read/writeaccesstoavariable,athreadwasstarted/stopped.AfterhavingemittedaneventthedebuggingVMcanbecon guredtosuspendexecutionandthusallowadeepviewintotheVM.Forexample:foreachcurrentlyrunningthreaditsstacktracecanbeanalysed.Foreachclasstheinnerstructurelikesuper-classesandimplementedinterfacescanberead.Eventhebytecodeofeverymethodcanbeaccessedforfurtheranalysis.

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

3.2jassdaandtheJDI

Asshownabove,theJDIallowsgeneratingeventsformanysituationsthatmightoccurduringtheexecutionofaJavasystem.ThemainfunctionofthecorelayerofthejassdaframeworkistodeterminewhicheventsarerequiredfortheanalysisofthegivenJavasystemandtocon gurethedebuggeesforthegenerationofthoseevents,only.Thesetofeventsrequiredforadebugrundependsontheinstalledmodulesandtheircon gurations.Theexecutionofadebugrunwiththejassdaframeworkcanbeseparatedintotwophases.

3.2.1InitialPhase

IntheinitialphasethejassdaframeworkconnectstothedebuggeesusingtheJDIandsuspendstheirexecution.Thentheloadedclassesarestaticallyanalysedinordertodeterminethesetofeventsthatmightbegeneratedduringtheirexecution.Afterthat,themodulesareaskedwhichoftheseeventstheyareinterestedin.Accordingly,thegenerationofthoseeventsiscon guredusingtheJDI.

3.2.2RuntimePhase

Afterhavingcon guredtheevents,theexecutionofthedebuggeesarere-sumed.Theexecutionissuspendedagainassoonasasituationofinterestoccursinoneofthedebuggeesandaneventisgenerated.Thebrokerreceivesthiseventanddistributesittothemodulesforfurtherprocessing.ThroughthedatatransferredwiththeeventthemoduleshavefullaccesstotheJDIandthereforemayperformanyactiontheJDIsupports,e.g.theycanreadandmanipulatethevaluesofvariablesor ndoutwhichsituationtriggeredthecurrentevent.

3.2.3HandlingDynamicClassLoading

AsJavasupportsloadingclassesdynamicallyduringruntime,eventsthatnotifyaboutloadingclassesareenabled.Inthiswaythejassdaframeworkkeepsinformedaboutnewclassesanditcon gurestheeventgenerationforthem,asdescribedfortheinitialphase.

3.2.4ObtainingReturn-ValuesofMethods

Formanyutilisationsofruntime-checkingobtainingthereturn-valueofamethodisofgreatimportance.Unfortunately,theJDIdoesnotsupportaccesstoreturn-valuesofmethods,directly.Forthejassdaframeworkwede-velopedasolutionto ndoutthatvaluewithouthavingtomodifytheJDIandthereforeloosethebene toftheplatform-independence.

Themainideaforaccessingthereturn-valueistowritethevalueintoaprivatevariableandgenerateaneventimmediatelybeforethemethodtermi-nates.Toachievethis,thejassdaframeworkprovidesaspecialclass-loaderthatpatchesthebytecodeofanymethodforwhichamodulerequiresthe

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

return-valueduringruntime.

4ProcessingExecutionEvents

Thejassdaframeworkprovidesaninfrastructurefordevelopingdebugger-applicationsthathavetomonitortheexecutionofJavasystems.Ahigh-levelinterfaceenablesthedevelopertopluginoneormoremodulesforprocessingtheeventsdeliveredbytheframework.Thesemodulesmustimplementtwobasicfunctions.Ontheonehandtheyhavetodecidewhicheventstheyareinterestedin,i.e.thealphabet.Thisisrequiredbythecorelayertocon gurethegenerationofeventsfromthedebuggees,accordingly.Ontheotherhandtheyneedtohandlethesequenceofeventsdeliveredbythebrokeronebyoneduringruntime.

4.1ModulesandAlphabets

Todeterminethealphabetofaregisteredmodule,themodulehastoproviderequestmethodsthatareusedbytheBroker.DuringstartupandwheneveranewclassisloadedtheBrokeraskseachmoduleifitisinterestedineventsemittedduringexecutionofthatclass.IncaseofpositiveresulttheBrokerrequestsalistofeventtypes8thatthemodulewantstoreceive.ConcerningthislisttheBrokeranalysesthenewclassandcreatesdummyeventsforalleventsthatcouldbelongtothemodule’salphabet.Inthe nalstepthemoduledecidesforallthesepossibleeventswhichdobelongtoitsalphabet.ThisdecisionisusedbytheBrokertocon gurethedebuggeesforeventemittingandfordispatchingtheeventsdeliveredbythedebuggeesduringruntime.

Thearchitectureofthejassdaframeworkincludesthecapabilityofrecon- gurationoftheeventemittingmechanism.Neweventscanbetriggered.Enabledeventscanbedisabledduringthedebugrun.Thisfeaturewillbeusedinfutureversionsofthejassdatool.

Currentlytherearetwomodulesavailable:theLoggermoduleandtheTrace-Checkermodule.Togetherwiththejassdaframeworktheyformthejassdatool.

4.2LoggerModule

TheLoggermoduleimplementsthefunctiontologtheexecutionofaJavasystembywritingitssequenceofeventsintoa le.Theamountofinformationthatcanbederivedfromaneventaswellasthealphabetcanbecon guredinanXML-basedcon guration le.

Figure3showssuchacon guration.Theoutputisdirectedtothe lesequence.logintheformatgivenbythetemplatede nition.Inthisde ni-tion eld-identi ersarereplacedbythepropertyvaluesofthereceivedevents.8TheseeventtypesaretakenfromtheJDI,e.g.methodentry,methodexit,etc.

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

<?xmlversion="1.0"encoding="UTF-8"?>

<logger>

<filename="sequence.log"/>

<event>

<template>%class%.%method%(%arguments%)=%returnvalue%</template>

</event>

<include>

<eventsetclass="jass.debugger.jdi.eventset.GenericSet"

field="class"

argument="jass.examples.*"/>

</include>

<exclude>

<eventsetclass="jass.debugger.jdi.eventset.GenericSet"

field="class"

argument="sun.*"/>

</exclude></logger>

Fig.3.Con gurationoftheLoggermodule

Theeventstoincludeandtoexcludearedeterminedbyhandlerclassesde- nedthroughtheclasspropertyofeventset.TheGenericSethandler,thatcomeswithjassdawillbesu cientinmostcases,butonemayalsowritetheirownevent lters.

ItwouldbeeasytowritesimilarmodulesthatwritethoseeventstoadatabaseviaJDBC,theJavadatabaseconnection.Inanycasetheloggeddatacanbeusedforanalysingtheprogram,e.g.inthewayitisdonebyKortenkampetal.in[13].Thereforewhenusingthismodule,jassdaperformscomparableoperationslikeothereventcollectingtools.

4.3Trace-CheckerModule

MorecomfortableistheuseofaCSPjassdaspeci cationtonotonlyreceiveeventsbutinadditiontoanalysethereceivedeventsonthe y.ThistracecheckingisverysimilartotraceassertionsinJass,butitisgeneralisedtoamoreexpressivelanguage.AmoredetailedviewontheCSPdialectCSPjassdaisgivenin[17]andintheappendix,butwithasmallexamplewewillillustratehowtodeterminetheTrace-Checker’salphabetfromagivenspeci cation.

In gure4thenormalbehaviourofappletsisspeci ed.The rstlinesde neeventsets.Eventsetsareusedtogroupevents.Oftenwedonotknowallpropertiesofaneventorsomeaspectsarenotrelevantinaspeci cation.Butthealphabetofthemoduleisnotdirectlybuiltbytheunionoftheseeventsets.

Thealphabetofthespeci cationisbuiltbythealphabetofthe rstprocessinthespeci cation–inthisexamplethealphabetofapplets()hastobeused.Tocalculatethisalphabetalleventsmentionedinthisprocessarecollected.Sincethisprocessisbuiltonaparallelcompositionoftheprocess

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

eventset

eventset

eventset

eventset

eventsetappletinitstartstopdestroy{{{{{instanceof="java.applet.Applet"}method="init"}method="start"}method="stop"}method="destroy"}

applets(){

||i:[instance]@appletbehaviour(i)

}

appletbehavior(inst){

applet.inst.init.begin->applet.inst.init.end

->appletrun(inst)

}

appletrun(i){

(applet.i.start.begin->applet.i.start.end

->applet.i.stop.begin->applet.i.stop.end->aplletrun(i)

)[]appletdestroy(i)

}

appletdestroy(inst){

applet.inst.destroy.begin->applet.inst.destroy.end->STOP}

Fig.4.CSPjassdaspeci cation“appletbehaviour”

appletbehaviour,itisnecessarytotaketheunionofallalphabetsofthesubprocessesforeachobjectinstance.

Thede nitionofappletbehaviourstartswiththe rsteventsetthatwehavetoaddtothealphabet.applet.inst.init.beginde nesaneventsetthatisbuiltbytheintersectionofthefourparts.appletde nesthesetofalleventsthatareemittedbyclassesthatareaninstanceofjava.applet.Applet.initde nesallevents redbymethodsnamedinit.beginisaprede nedeventsetdescribingalleventsofthemethodbegintype.Theeventsetinstistheparameteroftheprocess,itisunde nedwhencalculatingthealphabetandwillnotrestricttheeventset.Sothis rstexpressionde nesthesetofeventsthatare redwheneveramethodinitofanyinstanceofanappletbegins.

Continuingwiththiscalculationwewillendupinanalphabetofalleventstriggeredbyinvocationandnormalterminationofthemethodsinit,start,stopanddestroyforallinstancesofclassesextendingApplet.Toforbidcertaineventsduringthedebugrunitisalsopossibletostatethealphabetofaprocessexplicitly.

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

5BenchmarkExample

InordertogaininformationabouttheperformanceofthejassdatoolcheckingJavaapplications,asmallprogramisusedwhichsortsalistof10000numbersusingthebubblesortalgorithm.Thisprogramprovidestwoimplementationsofthealgorithm.The rstonecalculatesinonemethodandthereforerequiresonemethodinvocation.Thesecondimplementationputstheinnerloopintoaseparatemethodandrequires10001methodinvocations.Thebubblesortpro-gramisexecutedbytheSunJava1.3virtualmachine(inclassicandhotspotmode)andbytheSun1.4virtualmachineunderWindows2000onaPentium(1200MHz)system.Threedi erentcon gurationsarecompared:

(i)Theprogramisexecutedstandalonewithoutanymonitoring.

(ii)TheJavavirtualmachineiscon guredtorunindebug-mode

(iii)TheJavavirtualmachineiscon guredtorunindebug-modeandthe

jassdatoolisattachedloggingmethodinvocationsintoa le.methodinvocations(events)

standalonej2sdk1.3classic

j2sdk1.3hotspot

j2sdk1.4hotspot

debug-modej2sdk1.3classic

j2sdk1.3hotspot

j2sdk1.4hotspot

jassdaattachedj2sdk1.3classic

j2sdk1.3hotspot

j2sdk1.4hotspot

*withlessthan1%CPUusage19,2s1,0s1,0s39,0s10,7s1,1s40,2s11,2s*11,2s*100019,2s1,2s1,1s39,0s10,7s1,1s65,3s1805,3s*1804,0s*

Table1

Benchmarkresults

Asshownintable1thesortingof10000numbersinthestandalonecon- gurationrequires9,2sinclassicmodeandroundabout1sinhotspotmode.Enablingthedebug-modeincreasestheexecutiontimeoftheJava1.3VMbyupto10times.TheexecutiontimeoftheJava1.4VMkeepsalmostconstant,duetoitsfull-speeddebuggingsupport.AttachingthejassdatoolreducestheperformanceoftheJava1.3VMinclassicmodecomparedtothedebug-modebyfactor1.5.Thelasttwolinesshowthattheexecutiontimedramaticallyincreasesifthevirtualmachineisinhotspotmodeandhastohandlebreak-pointswhichthejassdatoolusesforindicationofmethodinvocations.InthiscasetheCPUusageisbelow1%whereasotherwise100%CPUusageisrequired.ThereasonforthelowCPUusageandlongexecutiontimeisstill

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

beeingexamined.

6Conclusion

Inthispaperwepresentedthemechanismofeventemittingusedinthejassdaframework.TheimplementationofaprototypehasproventhatthisisaviablemethodtodebugsomesmallJavaprograms.Buttheseexperimentshavealsoshownthelimitationsofourapproach.

Thejassdaframeworkworks ne,ifwecanreduceeventgenerationthroughthedynamicconceptof“ondemand”or“onthe y”generation.Todebugane cientalgorithmwithverylimitedcodetoexecutebetweenneededeventswillreducetheperformancedramatically.

Buttheaimwastohaveamethodtodebugdistributedsystemssothatthefocusliesoncommunicationevents.IncontrasttoJassthemotivationforthejassdatoolwasnottobeabletoperformDesignbyContractruntimechecks–althoughthismightpossiblybedonebynewmodulesinfutureversions.WhereasDesignbyContractassertionbuildthecounterpartofastatebasedspeci cationthejassdaframeworkshouldenableustobuildacounterpartforadynamicprocessbasedspeci cation.Forthisreasonweseejassdamoreasanadditiontostatebasedapproachesthanasareplacement.

Inadditionthelimitationscanalsobeseenasanadvantage:arunwithlowamountofeventsischeapandinthesamewayitischeaptoswitchthesetofeventsforasecondrun.Onlytheinitialphaseisin uencedbythenewsetofevents,butnobyte-codemodi cationisnecessaryeventhoughonlytheneededeventsforthesecondrunwillbegenerated.Sowepresumethatthejassdaframeworkwillhaveaconsiderableadvantageinenvironmentswhereeventsetsarelimitedbutdooftenchange.

6.1RelatedWork

TheideatoreducetheamountofeventstothosethatareneededinthecurrentdebugrunwasalreadyintroducedinMorphine[6]forprogramswritteninPROLOG.Butthecodefortheevent lteringforJavaprogramsisprovidedbytheJavavirtualmachine(VM)ofthesystem-under-test,sothatjassdadoesnothavetomodifythebytecodetoinsertstatementsorfunctioncallsforeventgeneration.

Forthesamereasonjassdadi ersfromJava-MaC[12],thatperformsex-actlythatbytecodemodi cation.Aprimitiveeventde nitionlanguageisusedtode ingthisde nitioneventgeneratingcodeisinsertedwhereneeded.Forthisreasonaneweventspeci cationmeansasecondpatchingoftheJavabytecode.

Theideaofaneventde nitionlanguage,thatseparatesthede nitionofeventsfromthesourcecode,wasalsogivenbyGatesetal.in[7].Butagainthistechniqueusesautomatedprograminstrumentationtogenerateevents

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

andthusdoesnotgeneratethemondemand.

6.2FutureWork

Besideatranslationfromacombinedspeci cationlanguagetotheinputlan-guageofthejassdaTrace-Checker,weplantocleanupthesourcecodeandprovideitasanOpenSourceprojectviathejassdahomepage9.

References

[1]Apt,K.-R.andE.-R.Olderog,“Veri cationofSequentialandConcurrentPrograms,”Springer-Verlag,1997,2ndedition.

[2]Bartetzko,D.,C.Fischer,M.M¨ollerandH.Wehrheim,Jass–JavawithAssertions,in:K.HavelundandG.Ro¸su,editors,ProceedingsoftheFirstWorkshoponRuntimeVeri cation(RV’01),Paris,France,July2001,ElectronicNotesinTheoreticalComputerScience55(2001).

[3]Br¨orkens,M.,“Trace-undZeit-ZusicherungenbeimProgrammierenmitVertrag,”Master’sthesis,Universit¨atOldenburg(2002),inGerman.

[4]Br¨orkens,M.andM.M¨oller,jassdaTraceAssertions,in:I.Schieferdecker,H.K¨onigandA.Wolisz,editors,TrendsinTestingCommunicatingSystems,InternationalConferneceonTestingCommunicatingSystems(TestCom),Berlin,Germany,2002,pp.39–48.

[5]Clarke,E.,E.EmersonandA.Sistla,Automaticveri cationof nitestateconcurrentsystemsusingtemporallogicspeci cations:Apracticalapproach,in:ConferenceRecordoftheTenthAnnualACMSymposiumonPrinciplesofProgrammingLanguages,ACM,1983,pp.117–126.

[6]Ducasse,M.andE.Jahier,E cientautomatedtraceanalysis:Exampleswithmorphine,in:K.HavelundandG.Rosu,editors,ProceedingsoftheFirstWorkshoponRuntimeVeri cation(RV’01),Paris,France,July2001,ElectronicNotesinTheoreticalComputerScience55(2001).

[7]Gates,A.Q.,S.Roach,O.MondragonandN.Delgado,Dynamics:Comprehensivesupportforrun-timemonitoring,in:K.HavelundandG.Rosu,editors,ProceedingsoftheFirstWorkshoponRuntimeVeri cation(RV’01),Paris,France,July2001,ElectronicNotesinTheoreticalComputerScience55(2001).

[8]Hoare,C.A.R.,Anaxiomaticbasisforcomputerprogramming,Comm.oftheACM12(1969),pp.576–580.

[9]Huisman,M.andB.Jacobs,Javaprogramveri cationviaaHoarelogicwithabrupttermination,in:T.Maibaum,editor,FASE2000:FundamentalApproachestoSoftwareEngineering,LectureNotesinComputerScience1783(2000),pp.284–303.

9

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

[10]Huzing,K.,R.KuuiperandSOOP,Veri cationofobject-orientedprograms

usingclassinvariants,in:T.Maibaum,editor,FASE2000:FundamentalApproachestoSoftwareEngineering,LectureNotesinComputerScience1783(2000),pp.208–221.

[11]Karaorman,M.,U.H¨olzleandJ.Bruno,jContractor:ARe ectiveJava

LibrarytoSupportDesignByContract,Technicalreport,DepartmentofComputerScience,UniversityofCalifornia,SantaBarbara(1998),http://www.cs.ucsb.edu/~murat/jContractor.PDF.[12]Kim,M.,S.Kannan,I.Lee,O.SokolskyandM.Viswanathan,Java-mac:arun-

timeassurancetoolforjavaprograms,in:K.HavelundandG.Rosu,editors,ProceedingsoftheFirstWorkshoponRuntimeVeri cation(RV’01),Paris,France,July2001,ElectronicNotesinTheoreticalComputerScience55(2001).

[13]Kortenkamp,D.,T.Milam,R.SimmonsandJ.L.Fernandez,Collectingand

analyzingdatafromdistributedcontrolprograms,in:K.HavelundandG.Rosu,editors,ProceedingsoftheFirstWorkshoponRuntimeVeri cation(RV’01),Paris,France,July2001,ElectronicNotesinTheoreticalComputerScience55(2001).

[14]Kramer,R.,iContract-theJavaDesignbyContracttool,Technicalreport,

ReliableSystems(1998),.

[15]Leavens,G.,A.BakerandC.Ruby,PreliminarydesignofJML:Abehavioral

interfacespeci cationlanguageforjava,Technicalreport,DepartmentofComputerScience,IowaStateUniversity(1998,revised2001).

[16]Meyer,B.,“Object-OrientedSoftwareConstruction,”ISE,1997,2ndedition.

[17]M¨oller,M.,SpecifyingandCheckingJavausingCSP,in:WorkshoponFormal

TechniquesforJava-likePrograms-FTfJP’2002,TechnicalReportNIII-R0204,ComputingScienceDepartment,UniversityofNijmegen,2002,(toappear).

[18]M¨uller,P.andA.Poetzsch-He ter,Modularspeci cationandveri cation

techniquesforobject-orientedsoftwarecomponents,in:G.T.LeavensandM.Sitaraman,editors,FoundationsofComponent-BasedSystems,CambridgeUniversityPress,2000(toappear).

[19]SunMicrosystems,JavaPlatformDebuggerArchitectureDocumentation

(1999),/products/jpda/doc/.

ACSPjassdaSemantics

Inthisappendixwewillbrie ydescribethebasicelementsofCSPjassdaandde netheoperationalsemantics,thatisusedduringruntimechecking.

A.1EventSets

Eventsetsarede nedbyanumberofproperties,i.e.keyvaluepairs,enclosedincurlybraces.ApropertynamedhandlerisrequiredtospecifyaJava

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

handlerclassthatisresponsiblefordecidingwhetheraJDIeventbelongstothecurrentsetornot.Otherpropertiesareadbythehandlerclasstocon gureit.

FormostcasestheclassGenericSet,thatcomeswiththejassdaTrace-Checkerwilldo ne.Thereforethisisthedefaultifnohandlerwasspeci ed.ThecurrentimplementationofGenericSetwillacceptanumberofproperties,e.g.tospecifytheclass,themethod,erde nedclassesarealsoallowedtobeusedashandlerclassesandthereforwillhavefullaccesstotheJDIevents.

Byusingtheeventsetkeywordeventsetsareboundtotheidenti erthatfollowsthekeyword.

Weallowintersection(“.”or“!”)andunion(“+”)ofeventsets.Thisallowsonetostatethatthecurrenteventshouldhavethepropertiesofbotheventsetsoritshouldhavethepropertiesofatleastoneeventset.

Finallyneweventsetscanbede ned“onthe y”duringthedebugrun.Wheneveraneventisaccepted(seenextsections),andthusisamemberofacurrenteventset,thepropertiesofthecurrenteventmaybeusedtode netheneweventset.Thisisdonebyaddinga“?”totheeventsetde nitionfollowedbythevariableidenti erandthemapping.Again,thismappingisdonebyahandlerclass,withMappingEventSetasdefaultimplementation.

Togiveanexampleweassumethatfirstandsecondarede nedeventsets.Thananeventsetfirst.second?third:[arg0="arg1"]willacceptalleventsthatbelongtobotheventsets,firstandsecond,andwhenaneventisacceptedaneweventsetwillbede nedwithidenti erthird,thatwillmatchalleventswitha rstargumentthatequalsthesecondargumentofthecurrentevent.

A.2Processes

CurrentlythejassdaTrace-Checkeracceptstwobasicprocesses:STOPandTERMwhereSTOPwillacceptnoeventandTERMwillonlyacceptterminationeventsofthedebuggees’virtualmachines.

Bypre xingaprocesswithaneventsetwede neanewprocess,that rstwillonlyacceptaneventbelongingtotheeventsetandthenbehavelikethepre xedprocess.

Syntax:

Process::=eventset->ProcessSemantics:

es->P →P

Externalchoicewillsplitsplitupthebehaviourintotwobranchesbutavoidsnondeterminism.

Syntax:

Process::=Process1[]Process2

whereev∈es

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

Semantics:

P →P ,¬ Q :Q →Q

P[]Q →P

evevevevQ →Q ,¬ P :P →P P[]Q →Q evevP →P ,Q →Q

P[]Q →P []Q

Quanti edexternalchoicewillbindaneweventsetvariable.

Syntax:

Process::=[]var:[map]Process1(var)

Semantics:

P(x) →P (x)

[]v:[map]P(v) →P (x)evwherex=map(ev)

Parallelcompositionisalwayssynchronisedovertheintersectionofalpha-betsofbothprocesses.Wewilluseα(P)asnotionforthealphabetofprocessP(theeventsaprocessisinterestedin).

Syntax:

Process::=Process1||Process2

Semantics:

P →P

P||Q →

evevP ||Q

P||Q

evwhereev∈α(P)\α(Q)whereev∈α(Q)\α(P)

whereev∈α(Q)∩α(P)Q →Q P||Q →ev

P →P ,Q →Q P||Q P||Q →

Analogoustoexternalchoicewede neaquanti edparallelcomposition.Semanticallyitisaparallelcompositionwhereforeachnewmappingresultwewillgetanewprocessinstance.

Syntax:

Process::=||var:[map]Process1(var)

Semantics:

||v:[map]P(v)

P(x) →P (x)

||Dv:mapP(v) →ev=|| v:mapP(v)wherex=map(ev)∧x∩D= P (x)||∪x||Dv:mapP(v)

Wheneveranamed(parameterised)processesisde nedtheprocessiden-ti ermaybeusedwhereaprocessisexpected.

Syntax:

ProcessDefinition::=Id(Params,...){[Alphabet;]Process}

Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level – either by inserting new source code prior to

Proccess::=ProcessId(Params,...)

Semantics:P →P

Id(p) →P

A.3TraceSemantics

ThejassdaTrace-Checkerwilltestduringruntimeifthetraceoftheprogram’seventsbelongstothetracesemanticsofthespeci cation.Theprocessofthe rstprocessde nitioninthespeci cationde nesthissemantics.

ThetracesemanticsofaprocessPisde nedbycollectingalleventse-quencesthatarepossiblewithrespecttotheoperationalsemantics.Sotheemptysequence isalwaysincludedandeveryinitialeventextendedbyanytraceofthesubsequentprocess.

traces(P)={ }∪{ ev atr| P :P →P ∧tr∈traces(P )}evevwhereprocess(Id(p))=P

本文来源：https://www.bwwdw.com/article/exoe.html