From: Nastaran Shafiei Date: Wed, 7 Mar 2018 22:06:52 +0000 (-0800) Subject: Uploaded wiki images. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=3f0145e38039475a1654974a45ad89c58e2e91e7 Uploaded wiki images. --- diff --git a/docs/graphics/DFSListener.svg b/docs/graphics/DFSListener.svg new file mode 100644 index 0000000..1684827 --- /dev/null +++ b/docs/graphics/DFSListener.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2005-10-21 18:50:44 +0000Canvas 1Layer 1searchStartedsearchFinishedstateAdvancedpropertyViolatedstateBacktrackedsearchConstraintHit diff --git a/docs/graphics/app-types.svg b/docs/graphics/app-types.svg new file mode 100644 index 0000000..f845707 --- /dev/null +++ b/docs/graphics/app-types.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2015-01-05 22:17:29 +0000App TypesLayer 1non-functional properties ■ unhandled exceptions (incl. AssertionError) ■ deadlocks ■ racesrestricted choice types ■ scheduling sequences ■ java.util.Random improved inspection ■ coverage statistics ■ exact object counts ■ execution costsconstraintsbenefitsrestricted application models ■ UML statemachines ■ does not run w/o JPF libraries runtime costs ■ order of magnitude slower ■ state storage memorystandard library support ■ java.net, javax.swing, .. (needs abstraction models) functional (domain) properties ■ built-in into JPF librariesfunctional property impl. costs ■ listeners, MJI knowledgeflexible state space ■ domain specific choices (e.g. UML "enabling events")runtime costs & library support ■ usually not a problem, domain libs can control state spaceruns on anyJVMruns onlyunder JPFlow modeling costs ■ statemachine w/o layout hassle,..initial domain impl. costs ■ domain libs can be tricky "sweet spot"annotate program ■ requirements ■ sequences (UML) ■ contracts (PbC) ■ tests … analyze program ■ symbolic exec → test data ■ thread safety / races *.class*.java@V*.javaJPF unawareprogramsJPF enabledprogramsJPF dependentprograms diff --git a/docs/graphics/attributes.svg b/docs/graphics/attributes.svg new file mode 100644 index 0000000..2aa20a4 --- /dev/null +++ b/docs/graphics/attributes.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-16 18:21:11 +0000Canvas 1Layer 1dup(), push(), pop(), ..------getOperandAttr(idx)setOperandAttr(idx,obj)getLocalAttr(idx)setLocalAttr(idx,obj)int[] localsObject[] localAttrint[] operandsObject[] operandAttrStackFramegetIntValue(idx), ...setIntValue(idx, v), ...------getFieldAttr(idx)setFieldAttr(idx,obj)getObjectAttr()setObjectAttr(obj)int[] valuesObject[] fieldAttrsObject objectAttrFieldslocalsvaluesattributesoperandsslotsfield-valuesattributesputfieldgetfielddup..iload..istore..invokevirtual..return..attributeobjectsetAttr(i,o)getAttr(i)- listener- Instruction- native peerget?Attr(i)set?Attr(i,o)JPF coreJPFextensionattribute APIobject-attrThreadInfoElementInfo diff --git a/docs/graphics/bc-factory.svg b/docs/graphics/bc-factory.svg new file mode 100644 index 0000000..f69c951 --- /dev/null +++ b/docs/graphics/bc-factory.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-16 18:32:22 +0000Canvas 1Layer 1*.classInstruction ifeq(tgt)...«interface»InstructionFactory...Instruction execute()InstructionIFEQIFEQ......Instruction execute (){.. cond = popCondition() if (cond) return jumpTarget else return getNextInsn()setCode(code)factoryInstruction[] codeMethodInfoconcrete execution semanticsabstract execution semanticsconcrete valueexecutionsymbolic valueexecutioninstruction setInstruction execute(){.. if (!firstStepInsn()){ setNextCG(new PCChoiceGenerator()) return this } popCondition() // not interested cond = getCG().getNextChoice() if (cond){... return jumpTarget } else {... return getNextInsn()per bytecodefactory methodsInstruction ifeq(tgt)...gov.nasa.jpf.jvm.bytecodeInstructionFactoryInstruction ifeq(tgt)...gov.nasa.jpf.symbcSymbolicInstructionFactoryInstruction ifeq(int jumpTarget){ return new IFEQ(jumpTarget)ClassInfoClassFileCodeBuilderConfigvm.insn_factory.class=... diff --git a/docs/graphics/cg-impl.svg b/docs/graphics/cg-impl.svg new file mode 100644 index 0000000..07a14cb --- /dev/null +++ b/docs/graphics/cg-impl.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-02 07:14:49 +0000Canvas 1Layer 1initNextTransition(){... curCg = nextCg nextCg = null curCg.advance() ..setExecThread() ...executeTransition(){.. isFirstStepInsn = true while (pc != null) { nextPc = executeInstruction() if (ss.breakTransition()) break else pc = nextPc isFirstStepInsn = falseexecute(){.. if (!ti.isFirstStepInsn()) { ChoiceGenerator cg = ..createMonitorEnterCG(..) if (cg != null){ ss.setNextChoiceGenerator(cg) return this // repeat } ei.lock(ti) return getNextPc(ti);execute()InstructioninitNextTransition()breakTransition()setNextChoiceGenerator()nextCgcurCgSystemStatehasMoreChoices()advance()ChoiceGeneratorgetNextChoice()threadSetThreadCGgetNextChoice()doubleSetDoubleCG......executeTransition()executeInstruction()isFirstStepInsn(){pc, nextPc}ThreadInfoMonitorEnterInvoke.....MethodInfoNativePeere.g. JPF_gov_nasa_jpf_vm_Verify.getBoolean(env)top half: executed on first invocationoptionally sets next CG and reexecutesbottom half: executed on revisit (orif no CG created because of policy)does semantic action based oncurrent CGs choicescheduling choicesdata acquisition choices123top halfbottomhalfif (!ti.isFirstStepInsn()){ cg = new BooleanCG() ss.setNextChoiceGenerator(cg) env.repeatInvocation() ..} else { cg = ss.getChoiceGenerator() return ((BooleanCG)cg).getNextChoice()}breakTransition(){... return nextCg != null diff --git a/docs/graphics/cg-motivation.svg b/docs/graphics/cg-motivation.svg new file mode 100644 index 0000000..e8c750c --- /dev/null +++ b/docs/graphics/cg-motivation.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2010-02-22 05:27:10 +0000Canvas 1Layer 1T ± Δ.. double v = Verify.getDouble("velocity"); ..velocity.class = gov.nasa.jpf.jvm.choice.DoubleThresholdGeneratorvelocity.threshold = 13250velocity.delta = 500application code(test driver)configuration (e.g. mode property file)C = { T-Δ, T, T+ Δ }Verify.getBoolean()Verify.getInt(0,4)Verify.getDouble(1.0,1.5)C = { true, false }C = { 0, 1, 2, 3, 4 }✓?potentially large sets with lots of uninteresting values??no finite value set without heuristicsC = { ∞ }e.g. "Threshold" heuristicChoice Generators+Configurable Heuristic Choice ModelsJPF internal object to store and enumerate a set of choicesconfigurable classes tocreate ChoiceGenerator instanceshasMoreChoices()advance()getNextChoice() → xchoiceSet: {x}xChoiceGenerator diff --git a/docs/graphics/cg-ontology.svg b/docs/graphics/cg-ontology.svg new file mode 100644 index 0000000..fab55e3 --- /dev/null +++ b/docs/graphics/cg-ontology.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2010-02-22 02:58:46 +0000Canvas 1Layer 1TransitionStateChoiceScheduling ChoiceData Choiceboolean b = Verify.getBoolean();double d = Verify.getDouble("MyHeuristic");..synchronized (..) {..}wait (..)x = mySharedObject..Control Choiceif (<cond>) ..INVOKECG.setInvocations(..).. diff --git a/docs/graphics/cg-sequence.svg b/docs/graphics/cg-sequence.svg new file mode 100644 index 0000000..5e0ff92 --- /dev/null +++ b/docs/graphics/cg-sequence.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2006-05-05 17:02:45 +0000Canvas 1Layer 1......get_field...monitor_enter...get_fieldmonitor_enter...ChoiceGeneratorTjTj+1Tj+2CGkCGlsetNextCGgetNextChoiceTransitionc1kc2kc3kSkc1kc2k{{}},==Statebacktrackadvancec2k,c1l...,execute{Instruction}Sl diff --git a/docs/graphics/choicegen-example.svg b/docs/graphics/choicegen-example.svg new file mode 100644 index 0000000..675ec8d --- /dev/null +++ b/docs/graphics/choicegen-example.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2006-05-03 17:51:17 +0000Canvas 1Layer 1T ± Δ.. double v = Verify.getDouble("velocity"); ..velocity.class = DoubleThresholdvelocity.threshold = 13250velocity.delta = 500application code(test driver)configuration (e.g. mode property file)C = { T-Δ, T, T+ Δ }Verify.getBoolean()Verify.getInt(0,4)Verify.getDouble(1.0,1.5)C = { true, false }C = { 0, 1, 2, 3, 4 }✓?potentially large sets with lots of uninteresting values??no finite value set without heuristicsC = { ∞ }e.g. "DoubleThresholdChoice"Choice Generators+Configurable Heuristic Choice ModelsJPF internal object to store and enumerate a set of choicesconfigurable classes tocreate ChoiceGenerator instanceshasMoreChoices()advance()getNextChoice() → xchoiceSet: {x}xChoiceGenerator diff --git a/docs/graphics/genpeer.svg b/docs/graphics/genpeer.svg new file mode 100644 index 0000000..6887428 --- /dev/null +++ b/docs/graphics/genpeer.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-04 01:29:55 +0000Canvas 1Layer 1GenPeerpackage x.y.z;class MyClass { ... native String foo (int i, String s);}class JPF_x_y_z_MyClass { ... @MJI public static int foo__ILjava_lang_String__2 (MJIEnv env, int objRef, int i, int sRef) { int ref = MJIEnv.NULL; // <2do> fill in body return ref; }}"java gov.nasa.jpf.GenPeer x.y.z.MyClass > JPF_x_y_z_MyClass.java" diff --git a/docs/graphics/interleavings.svg b/docs/graphics/interleavings.svg new file mode 100644 index 0000000..4dfa19e --- /dev/null +++ b/docs/graphics/interleavings.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-11-19 20:18:08 +0000Canvas 1Layer 1.........12P1P2PNn1n2...AtomicInstructionsThreads12I1∑niIM......nN.........Interleavings(∑ n )!∏ (n !)Ni=1iNi=1iM = diff --git a/docs/graphics/jpf-abstractions.svg b/docs/graphics/jpf-abstractions.svg new file mode 100644 index 0000000..b636c6f --- /dev/null +++ b/docs/graphics/jpf-abstractions.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-11-26 21:24:31 +0000Canvas 1Layer 1search ()VM vmSearchforward ()backtrack ()restoreState ()VMsearch ()DFSearchrun ()search, vm, configJPFexecuteTransition ()executeInstruction ()ThreadInfoinitializeNextTransition()executeNextTransition()SystemStateClassInfoMethodInfoFieldInfoElementInfoFieldsMonitorStaticsbytecode executiontype + codemgntobjectmodelgov.nasa.jpfgov.nasa.jpf.searchsearch ()HeuristicSearchgov.nasa.jpf.vmgov.nasa.jpf.search.heuristicgov.nasa.jpf.vm.bytecodeexecute ()Instruction.........search ()BFSHeuristic...while (notDone) { ..vm.forward(); ..vm.backtrack(); if (!properties.check()){ reportError(); break; ...search.class=...vm.class=...push (), pop() ...StackFrameConfigHeap diff --git a/docs/graphics/jpf-basic.svg b/docs/graphics/jpf-basic.svg new file mode 100644 index 0000000..fdfae11 --- /dev/null +++ b/docs/graphics/jpf-basic.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-11-19 18:37:23 +0000Canvas 1Layer 1JPF*.classreport*.jpfSystem under Test(Java bytecode)Verification ResultJPF ConfigurationProperties to Verify diff --git a/docs/graphics/jpf-intro-new.svg b/docs/graphics/jpf-intro-new.svg new file mode 100644 index 0000000..56fc211 --- /dev/null +++ b/docs/graphics/jpf-intro-new.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2009-04-10 01:07:23 +0000Canvas 1Layer 1------------------------------------ error path..Step #14 Thread #1 oldclassic.java:95 event2.waitForEvent(); oldclassic.java:37 wait();------------------------------------ thread stacksThread: Thread-0 at java.lang.Object.wait(Object.java:429) at Event.waitForEvent(oldclassic.java:37) ..======================== 1 Error Found: DeadlockJPFCorebytecodesetlistener/propertypublisher/ -extchoicegeneratorserializer/restorerannotation (optional) in-sourceproperty specdomainframeworkmodellibraryapplicationSuTexecutionenvironmentsearchstrategyJavavirtualmachinebytecodereportJPFendseenerror-pathproperty violationhost - JVMJPF distribution...nativepeer......extensions*.jpfJPF configurationreportstandardJava libraries*.jar*.jar diff --git a/docs/graphics/jpf-layers.svg b/docs/graphics/jpf-layers.svg new file mode 100644 index 0000000..ada4957 --- /dev/null +++ b/docs/graphics/jpf-layers.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-02 21:48:18 +0000Canvas 1Layer 1platform OShost JVMnative librarieslibrary classesJPF (Java application)modeled classesrt.jarJNIMJI*.classsystem under teststandard Java installationCLASSPATHModel layerJava layerNative layer"Java Native Interface""Model Java Interface" diff --git a/docs/graphics/jpf-project.svg b/docs/graphics/jpf-project.svg new file mode 100644 index 0000000..790b51b --- /dev/null +++ b/docs/graphics/jpf-project.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2009-09-09 23:36:00 +0000Canvas 1Layer 1jpf-Xsrcbuildbuild.xmljpf.propertiesX.jarX-classes.jarX-annotations.jarmainpeersclassesannotationstestsexampleslibtoolsbinRunJPF.jarRunAnt.jarjpfantnbprojectproject.xmlide-file-targets.xml.classpathmainpeersclassesannotationstestsexampleseclipserun-jpf.launchJPF project properties file(runtime def: native_classpath, classpath, sourcepath)host-VM executed classes (listeners, infrastructure etc.)host-VM executed library classes (MJI native peers)JPF executed library classes →sourcepathJPF processed Java annotationsregression testsdemos →sourcepathAnt build script (compile, build, test, clean)temporary build artifacts (classfiles)main host-VM executed project jar (main,peers →native_classpath)JPF executed library jar (classes,annotations →classpath)separate anotations jar (for JPF external SUT exec)required runtime jars →native_classpathbuild toolsant.jar, junit.jar, ...bcel.jar, antlr.jar, ..(example) 3rd party jarsbuild artifactspermanent build artifacts(example) 3rd party jarsJPF startup jar (executable)JPF build jar (executable)scriptsJPF startup script (→RunJPF.jar)JPF build script (→RunAnt.jar)Eclipse project configurationproject sourcesproject root directorybinary distributionNetBeans project configurationNetBeans file actions (JPF execution)Eclipse launch configs (JPF execution)IDE supportcompilebuildtest diff --git a/docs/graphics/listener-overview.svg b/docs/graphics/listener-overview.svg new file mode 100644 index 0000000..8a58bd9 --- /dev/null +++ b/docs/graphics/listener-overview.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-02 07:42:37 +0000Canvas 1Layer 1SearchVMJPFSystem under testlistenersexecuted by JPFexecuted by host JVMsearch event notificationsexecution event notificationsconfigured- classLoaded (vm)- threadScheduled (vm)- threadNotified (vm) ...- executeInstruction (vm)- instructionExecuted (vm) ...- objectCreated (vm) ...- exceptionThrown(vm) ...- choiceGeneratorAdvanced (vm) ...- stateAdvanced (search)- stateBacktracked (search)- propertyViolated (search)- searchFinished (search) ...- +listener=<listener-class>- @JPFConfig(..)- listener.autoload=<annotations>- jpf.addListener(..) ...≪SearchListener≫≪VMListener≫ diff --git a/docs/graphics/listeners.svg b/docs/graphics/listeners.svg new file mode 100644 index 0000000..681d1ad --- /dev/null +++ b/docs/graphics/listeners.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2009-04-08 19:52:28 +0000Canvas 1Layer 1«interface»JPFListenerexecuteInstruction(vm)instructionExecuted(..)threadStarted(..)objectCreated(..)choiceGeneratorSet(..)choiceGeneratorAdvanced(..). . .«interface»VMListenersearchStarted(search)stateAdvanced(..)stateBacktracked(..)propertyViolated(..)searchFinished(..). . .«interface»SearchListenercheck(search,vm)getErrorMessage()«interface»Propertycheck(search,vm) {}. . .GenericPropertyinstructionExecuted(vm) {}searchStarted(search) {}. . .ListenerAdapterpublishStart(publisher)publishFinished(..). . .«interface»PublisherExtensioninstructionExecuted(vm) {}searchStarted(search) {}. . .PropertyListenerAdapter diff --git a/docs/graphics/mji-call.svg b/docs/graphics/mji-call.svg new file mode 100644 index 0000000..d5db418 --- /dev/null +++ b/docs/graphics/mji-call.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-24 04:08:50 +0000Canvas 1Layer 1package x.y.z;class C { ... native int foo (int p);}class JPF_x_y_z_C { ... public static int foo__I__I (MJIEnv env, int thisRef, int p) { int d = env.getIntField(thisRef, "data"); .. }}...int a = c.foo(3);...aload_1icont_3invokevirtual ..executeMethod (ThreadInfo ti..){ MJIEnv env = ti.getMJIEnv(); Object[] args = getArguments(); .. mth.invoke(peerCls, args); ..}ClassInfo (..){ peerCls = loadNativePeer(..); ..}executeMethod()peerClsClassInfoexecuteMethod()methodsNativePeergetXField(..)setXField(..)...threadInfoMJIEnvenvThreadInfoJPFclassloadingJPFmethodinvocationJPFobjectaccessJPF (model) classJVM (Java) classJava reflection callreflection diff --git a/docs/graphics/mji-functions.svg b/docs/graphics/mji-functions.svg new file mode 100644 index 0000000..bac9b5c --- /dev/null +++ b/docs/graphics/mji-functions.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-24 04:01:26 +0000Canvas 1Layer 1class JPF_x_y_z_MyClass { public static int foo__ILjava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int i, int sRef) { String s = env.getStringObject(sRef); .. int ref = env.newString(..); return ref; }}package x.y.z;class MyClass { .. native String foo (int i, String s);}MJIEnvJPF objectsJava objectsNativePeerJPF executedhost VM executed- method lookup- parameter conversion- invocation- field access- object conversion- JPF intrinsics access"Model" Class"NativePeer" ClassMJI - "Model Java Interface" diff --git a/docs/graphics/mji-mangling.svg b/docs/graphics/mji-mangling.svg new file mode 100644 index 0000000..7e59270 --- /dev/null +++ b/docs/graphics/mji-mangling.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-02 21:54:02 +0000Canvas 1Layer 1package x.y;class MyClass { native int foo (int i, String s);}class JPF_x_y_MyClass { public static int foo__ILjava_lang_String_2 (MJIEnv env, int objref, int i, int sRef) {..}}Model ClassNative Peer Classmodel parameters(refs become 'int')MJI parametersJNI conformant manglingbooleanbytecharshortintlongfloatdoubleZBCSIJFD'_'';''['_1_2_3<type> [][<type>x.y.ZLx_y_Z_2<func> (..)<func>__<signature> diff --git a/docs/graphics/new-testing.svg b/docs/graphics/new-testing.svg new file mode 100644 index 0000000..4254ad1 --- /dev/null +++ b/docs/graphics/new-testing.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-05 00:34:03 +0000Canvas 1Layer 1@Test public void testX() { if (verifyNoPropertyViolation()) { String s = "one" + " two"; assert "one two".equals(s); }}boolean verifyNoPropertyViolation (String... jpfArgs) { ... args = append(jpfArgs, caller.getClassName(), caller.getMethodName()); .. JPF jpf = createAndRunJPF(args); ... errors = jpf.getSearchErrors(); if (!errors.isEmpty()) throw new AssertionError(..); ... return false; // -> don't execute test block}boolean verifyNoPropertyViolation(..){ return true;}start()JPFShellrunTestsOfThisClass()createAndRunJPF()...verifyNoPropertyViolation()verifyPropertyViolation()verifyUnhandledException()verifyAssertionError()...TestJPFtestX()...MyJPFProjectTestjpf-coretested JPF projectverifyNoPropertyViolation()verifyPropertyViolation()verifyUnhandledException()verifyAssertionError()JPF_.._TestJPFnative peercode verified by JPFexecuted by JPF whenrunning testexecuted outside JPF (starting JPF on test) diff --git a/docs/graphics/por-mark.svg b/docs/graphics/por-mark.svg new file mode 100644 index 0000000..f47b060 --- /dev/null +++ b/docs/graphics/por-mark.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-12-02 07:35:36 +0000Canvas 1Layer 1XX1XX12Xstatic fieldsT1T2root setheapphase 1phase 21 & 2 : referencing thread numberX : shared diff --git a/docs/graphics/por-scheduling-relevance.svg b/docs/graphics/por-scheduling-relevance.svg new file mode 100644 index 0000000..45c2886 --- /dev/null +++ b/docs/graphics/por-scheduling-relevance.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-11 18:17:44 +0000Canvas 1Layer 1executed bytecode instructionfield insnsync insninvoke insnsync mththreading callscheduling relevant insn typeother runnable threadsrecursive locksshared objectslock protected accessscheduling relevant instruction (registeres a ThreadChoiceGenerator)data racesdeadlocks(lock races)tracking of access threadslock distance & statisticsThread. start(), yield() sleep(), join()Object.wait(),notify()configuredclass/mthdattributesGETFIELDPUTFIELDGETSTATICPUTSTATICxALOADxASTOREMONITORENTERMONITOREXITINVOKEVIRTUALINVOKESTATIC diff --git a/docs/graphics/properties.svg b/docs/graphics/properties.svg new file mode 100644 index 0000000..ad56b87 --- /dev/null +++ b/docs/graphics/properties.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2011-05-11 18:07:23 +0000Canvas 1Layer 1jpf.home = ${user.home}/projects/jpfjpf-core = ${jpf.home}/jpf-corejpf-awt = ${jpf.home}/awtjpf-shell = ${jpf.home}/jpf-shelljpf-aprop = ......extensions = ${jpf-core},${jpf-shell}jpf-core = ${config_path}jpf-core.native_classpath=\ ${jpf-core}/build/jpf.jar;\ ... ${jpf-core}/lib/bcel.jar;jpf-core.classpath=\ build/jpf-classes.jarjpf-core.test_classpath=\ build/testsjpf-core.sourcepath=\ src/classes...jpf-awt-shell = ${config_path}@using = jpf-awtjpf-awt-shell.native_classpath=...jpf-awt-shell.classpath=......target = RobotManagertarget_args = ...@using = jpf-aprop@import = ./my.propertiesshell = .shell.basicshell.BasicShelllistener = .aprop.listener.SharedChecker...1. site properties2. project properties3. application properties4. command line~/.jpf/site.properties<project>/jpf.properties<project>/.../*.jpf> bin/jpf [-log][-show] {+log.info=..} .../RobotManager.jpf all jpf.properties inorder of extensionsjpf.properties in current directory- project locations- pre-loaded projects- project class paths- project dependencies- system-under-test- listeners, shells- debuggingcommand line property arguments...applicationpropertiessite properties diff --git a/docs/graphics/report.svg b/docs/graphics/report.svg new file mode 100644 index 0000000..cad3324 --- /dev/null +++ b/docs/graphics/report.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2010-09-10 23:02:45 +0000Canvas 1Layer 1JPF()addPublisherExtension()setPublisherTopics()reporterJPF..reporter = config.getInstance("report.class", Reporter.class,..);..searchStarted()propertyViolated()searchFinished()publishersReporterpublishStart()getOut()extensionstopicsoutPublisherpublishStart()publishTransition()publishPropertyViolation()publishFinished()<<PublisherExtension>>........for (Publisher p : publishers){ p.openChannel(); .. p.publishStart();.. public void publishStart() { for (String topic : startTopics) { if ("jpf".equals(topic)){ publishJPF(); ... for (PublisherExtension e : extensions) { e.publishStart(this); } ...out.println("JPF version" + ..);publishJPF()...ConsolePublisherpublishFinished()...DeadlockAnalyzerPrintWriter out = publisher,getOut();printTraceAnalysis(out);data collectionpublisher managementdata formattingtopic managementoutput channel managementproperty/listenerspecific output topicsreport.class=.report.Reporterreport.publisher=console,..report.console.class=.report.ConsolePublisherreport.console.start=jpf,..JPF configuration(e.g. jpf.properties or *.jpf files) diff --git a/docs/graphics/states-mc.svg b/docs/graphics/states-mc.svg new file mode 100644 index 0000000..8d9f5fd --- /dev/null +++ b/docs/graphics/states-mc.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2009-09-06 18:37:27 +0000Canvas 1Layer 1☠model checking:all program state are explored until none left or defect foundbacktrack≡≡≡match✘ diff --git a/docs/graphics/states-testing.svg b/docs/graphics/states-testing.svg new file mode 100644 index 0000000..12e5396 --- /dev/null +++ b/docs/graphics/states-testing.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-11-19 20:33:35 +0000Canvas 1Layer 1☠based on input set {d}only one pathexecuted at a time✔testing:{d} diff --git a/docs/graphics/sw-model-checking-2.svg b/docs/graphics/sw-model-checking-2.svg new file mode 100644 index 0000000..a0575f7 --- /dev/null +++ b/docs/graphics/sw-model-checking-2.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2015-01-05 22:19:29 +0000Canvas 1Layer 1a=0b=0b=1b=2c=0c=0c=0/0starta=1b=0b=1b=2c=-1c=1/0c=1✘12345✔✔6 diff --git a/docs/graphics/sw-model-checking.svg b/docs/graphics/sw-model-checking.svg new file mode 100644 index 0000000..1fd0a54 --- /dev/null +++ b/docs/graphics/sw-model-checking.svg @@ -0,0 +1,3 @@ + + + Produced by OmniGraffle 6.1 2014-11-19 20:40:12 +0000Canvas 1Layer 1Random random = new Random() int a = random.nextInt(2)int b = random.nextInt(3)int c = a/(b+a -2)①②③④a=0b=0b=1b=2c=0c=0c=0/0starta=1b=0b=1b=2c=-1c=1/0c=1✔