Difference between revisions of "MCInstrumentation"

From BP Wiki
Jump to: navigation, search
Line 10: Line 10:
 
* Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.
 
* Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.
  
== pruneSearchNow()==  
+
== pruneSearchNow()==
  
 
* Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined.
 
* Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined.
  
== pruneAtNextVerificationState() ==  
+
== pruneAtNextVerificationState() ==
 
* forces backtracking after all b-threads reach the next state and after its badness is determined.
 
* forces backtracking after all b-threads reach the next state and after its badness is determined.
  
== labelNextVerificationState(…) ==  
+
== labelNextVerificationState(…) ==
 
* Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product).
 
* Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product).
 
* When BPmc reaches a BP-state that was already fully checked – it backtracks.
 
* When BPmc reaches a BP-state that was already fully checked – it backtracks.
* If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product.
+
* If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product. For example, a logger b-thread that does not request events and does not affect the outcome of the run, does not have to label its states. 
 +
* A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
 +
* The states of a "linear" b-threads can be just numbered as 1/2/3 etc.. The states of a more complex b-thread can be labeled based on the values of the variables that determine the state change.

Revision as of 14:37, 4 August 2013

= Application Instrumentation and Assistance in BPmc

The following API calls can be used inside Java b-thread to control the model checking process. Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.

markNextVerificationStateAsBad()

  • Indicates safety property violation. MC stops and prints a counterexample.

markNextVerificationStateAsHot()

  • Used for liveness property checking. BPmc looks for reachable cycles that contains only hot states (and no cold states). By default, states are considered cold.

pruneSearchNow()

  • Forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined.

pruneAtNextVerificationState()

  • forces backtracking after all b-threads reach the next state and after its badness is determined.

labelNextVerificationState(…)

  • Optionally provides a label for a b-thread state, to be used in constructing the BP-state (concatenating all bt-states - creating their Cartesian product).
  • When BPmc reaches a BP-state that was already fully checked – it backtracks.
  • If a b-thread does not label any of its states – it is considered to have one state – and it does not increase the size of the Cartesian product. For example, a logger b-thread that does not request events and does not affect the outcome of the run, does not have to label its states.
  • A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
  • The states of a "linear" b-threads can be just numbered as 1/2/3 etc.. The states of a more complex b-thread can be labeled based on the values of the variables that determine the state change.