EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » LAB 4
Trace:
lab4

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
lab4 [2017/01/27 20:11] – francklab4 [2017/01/30 13:56] (current) – franck
Line 1: Line 1:
 +~~NOTOC~~
 +
 +====== LAB 4 ======
 +
 ====== Listeners ====== ====== Listeners ======
 +
  
 Choose one of the following listeners (please don't all choose the first one).  Write one or more sample programs to illustrate the use of the listener.  Some listeners have associated properties.  Illustrate their use as well.  Describe the listener and its properties.  The source code of the listeners can be found in jpf-core/src/main/gov/nasa/jpf/listener/ Choose one of the following listeners (please don't all choose the first one).  Write one or more sample programs to illustrate the use of the listener.  Some listeners have associated properties.  Illustrate their use as well.  Describe the listener and its properties.  The source code of the listeners can be found in jpf-core/src/main/gov/nasa/jpf/listener/
Line 64: Line 69:
       * vt.methods       * vt.methods
  
- To receive feedback, submit your work as a text file using the submit command before Tuesday January 31:+ To receive feedback, submit your work as a text file using the submit command before Tuesday January 31:\\
 submit 4315 lab4 <name of the listener>  submit 4315 lab4 <name of the listener> 
  
Line 80: Line 85:
 To illustrate the BudgetChecker listener, we consider the following app. To illustrate the BudgetChecker listener, we consider the following app.
  
 +<code java>
 import java.util.ArrayList; import java.util.ArrayList;
 import java.util.List; import java.util.List;
Line 93: Line 99:
     }     }
 } }
 +</code>
  
 We can run the listener BudgetChecker without setting any of its properties We can run the listener BudgetChecker without setting any of its properties
 and, hence, not setting any constraints, as shown in the application properties file below. and, hence, not setting any constraints, as shown in the application properties file below.
  
 +<code>
 target=Constraints  target=Constraints 
 classpath=. classpath=.
 cg.enumerate_random=true cg.enumerate_random=true
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 +</code>
  
 In this case, no constraints are set.  As a result, JPF will run out of memory producing In this case, no constraints are set.  As a result, JPF will run out of memory producing
 the following output the following output
  
 +<code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 113: Line 123:
 ====================================================== search started: 1/27/17 1:01 PM ====================================================== search started: 1/27/17 1:01 PM
 [SEVERE] JPF out of memory [SEVERE] JPF out of memory
 +...
 +</code>
  
 We can constrain the maximum amount time used by JPF to 1000 milliseconds as follows. We can constrain the maximum amount time used by JPF to 1000 milliseconds as follows.
 We can assign any long value to the property budget.max_time. We can assign any long value to the property budget.max_time.
  
 +<code>
 target=Constraints target=Constraints
 classpath=. classpath=.
Line 122: Line 135:
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 budget.max_time=1000 budget.max_time=1000
-  +</code> 
 Since JPF cannot complete within one second, it stops after one second and produces the following output.  Since JPF cannot complete within one second, it stops after one second and produces the following output. 
  
 +<code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 135: Line 150:
 ====================================================== search constraint ====================================================== search constraint
 max time exceeded: 00:00:01 >= 00:00:01 max time exceeded: 00:00:01 >= 00:00:01
 +...
 +</code>
  
 The amount heap space used by JPF can be constrained to a maximum number of bits as follows. The amount heap space used by JPF can be constrained to a maximum number of bits as follows.
 We can assign any long value to the property budget.max_heap. We can assign any long value to the property budget.max_heap.
  
 +<code>
 target=Constraints target=Constraints
 classpath=. classpath=.
Line 144: Line 162:
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 budget.max_heap=10000000 budget.max_heap=10000000
 +</code>
  
 Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes.  Since Note that 10000000 bits = 10000000 / (1024 * 1024) megabytes = 9.5 megabytes.  Since
 JPF needs more heap space, it stops and produces the following output. JPF needs more heap space, it stops and produces the following output.
  
 +<code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 159: Line 178:
 ====================================================== search constraint ====================================================== search constraint
 max heap exceeded: 10MB >= 9MB max heap exceeded: 10MB >= 9MB
 +...
 +</code>
  
 One can constrain JPF from checking more than 100 bytecode instructions as follows. One can constrain JPF from checking more than 100 bytecode instructions as follows.
-We can assign any int value to the property budget.max_insn.+We can assign any long value to the property budget.max_insn.
  
 +<code>
 target=Constraints target=Constraints
 classpath=. classpath=.
Line 168: Line 190:
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 budget.max_insn=100 budget.max_insn=100
 +</code>
  
 Since this constraint is violated, JPF produces the following output. Since this constraint is violated, JPF produces the following output.
  
 +<code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 181: Line 205:
 ====================================================== search constraint ====================================================== search constraint
 max instruction count exceeded: 100 max instruction count exceeded: 100
 +...
 +</code>
  
 +We can also limit the number of states that JPF explores by setting the property budget.max_state.  We can assign any int value to this property. 
  
 +<code>
 target=Constraints target=Constraints
 classpath=. classpath=.
Line 188: Line 216:
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 budget.max_state=100 budget.max_state=100
 +</code>
  
 +Since the statespace of this app consists of more than 100 states, JPF stops and produces the following output.
  
- +<code>
- +
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 203: Line 231:
 ====================================================== search constraint ====================================================== search constraint
 max states exceeded: 100 max states exceeded: 100
 +...
 +</code>
  
 +We can also constrain the depth of the search.  The corresponding property, budget.max_depth, can take any int value.
 +
 +<code>
 target=Constraints target=Constraints
 classpath=. classpath=.
Line 209: Line 242:
 listener=gov.nasa.jpf.listener.BudgetChecker listener=gov.nasa.jpf.listener.BudgetChecker
 budget.max_depth=100 budget.max_depth=100
 +</code>
  
 +Since the depth of the search is greater than 100 for this app, JPF stops and produces the following output.
  
 +<code>
 JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved. JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
  
Line 221: Line 257:
 ====================================================== search constraint ====================================================== search constraint
 max search depth exceeded: 100 max search depth exceeded: 100
 +...
 +</code>
 +
  
lab4.1485547861.txt.gz · Last modified: 2017/01/27 20:11 by franck