BPJ Model Checking API - Revision history

BpAdmin: /* BPJ Model Checking API: Enabling your application for model-checking and controlling its verification */

2014-03-19T09:45:15Z

‎BPJ Model Checking API: Enabling your application for model-checking and controlling its verification

BpAdmin: BPmcAPI moved to BPJ Model Checking API

2014-03-19T09:42:32Z

BPmcAPI moved to BPJ Model Checking API

Assaf: /* BPmc API: Controlling model checking from your application */

2014-02-11T13:42:01Z

‎BPmc API: Controlling model checking from your application

Assaf: /* setBThreadEpsilon() */

2014-02-11T13:37:54Z

‎setBThreadEpsilon()

Assaf: /* BPmc API: Controlling model checking from your application */

2014-02-11T13:36:05Z

‎BPmc API: Controlling model checking from your application

Assaf: /* setBThreadEpsilon(double) */

2014-02-11T12:50:51Z

‎setBThreadEpsilon(double)

Assaf at 12:50, 11 February 2014

2014-02-11T12:50:19Z

Assaf: /* labelNextVerificationState() */

2014-02-11T12:40:00Z

‎labelNextVerificationState()

Assaf: /* labelNextVerificationState() */

2014-02-11T12:38:07Z

‎labelNextVerificationState()

Assaf: /* labelNextVerificationState() */

2014-02-11T12:37:30Z

‎labelNextVerificationState()

@@ Line 1: / Line 1: @@
-= BPmc API: Enabling your application for model-checking and controlling its verification =
+= Enabling your application for model-checking and controlling its verification =
 Before verifying an application, the application must be enabled for model checking.
@@ Line 21: / Line 21: @@
 * It is the programmer's responsibility to disambiguate all relevant b-thread states of each relevant b-thread.
 * The (composite) BP-state name is the concatenation all constituent bt-states.
-* When BPmc reaches a BP-state that was already fully checked – it backtracks.
+* When BPJ model checking reaches a BP-state that was already fully checked – it backtracks.
 * If a b-thread does not label its states – it is considered to have one state – and it does not increase the size of the Cartesian product. E.g. a b-thread that only counts events theoretically has infinitely many states. However, if this b-thread is known to never request or block events, it cannot affect the application flow, and if the counts do not matter in the counterexamples, there is no need to keep track of its exact state during back tracking.
 * A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
 * Meaningful state names can help in debugging, but since since most b-threads are simple this is not critical. E.g., the states of a "linear" b-thread can be just numbered as 1/2/3 etc. The states of a b-thread can be labeled also based on the values of the variables that determine the state change.
-* State names are local to the b-thread and must be unique only within a b-thread. The BPmc infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.
+* State names are local to the b-thread and must be unique only within a b-thread. The BPJ model checking infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.
 == markNextVerificationStateAsBad()==
-Indicates detection by the b-thread of a violation of a safety property. BPmc stops and prints the sequence of events (the path) to this point as a counter example.
+Indicates detection by the b-thread of a violation of a safety property. Model checking stops and prints the sequence of events (the path) to this point as a counter example.
 == markNextVerificationStateAsHot()==
-This call is used for checking of liveness properties. States that are not marked as hot are considered cold. If BPmc detects a cycle in the state graph that does not contain a cold state, it stops and prints the path to this cycle and the cycle as a counter example.
+This call is used for checking of liveness properties. States that are not marked as hot are considered cold. If  the model checking detects a cycle in the state graph that does not contain a cold state, it stops and prints the path to this cycle and the cycle as a counter example.
 == pruneSearchNow()==
 This forces backtracking immediately, possibly stopping other b-threads and possibly before the badness of the next state is determined. This call can be used by a b-thread to accelerate the model checking by eliminating states that weren't explored, but are known to lead to results that are known or are symmetric to other states, or are otherwise not relevant in the present run.

@@ Line 1: / Line 1: @@
-= BPmc API: Controlling model checking from your application =
+= BPmc API: Enabling your application for model-checking and controlling its verification =
 Before verifying an application, the application must be enabled for model checking.
 This includes at least:
 * Creating b-threads which simulate the environment, when applicable.
 * Assigning names to states
 * Determining alternative execution paths - by identifying equal priority b-threads and equal priority event requests.

← Older revision		Revision as of 13:37, 11 February 2014
Line 37:		Line 37:

	== setBThreadEpsilon(<double epsilon>) ==		== setBThreadEpsilon(<double epsilon>) ==
−	This call defines ~~non-determinism~~ between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of ~~non-deterministic~~ execution, backtracking and exploration of alternative execution paths.	+	This call defines nondeterminism between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of nondeterministic execution, backtracking and exploration of alternative execution paths.

@@ Line 1: / Line 1: @@
 = BPmc API: Controlling model checking from your application =
 B-threads can call the following API methods of the BProgram where the b-thread is added/registered
 to control the model checking.
-Throughout, the term nextVerificationState refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.
+Throughout, the term Next Verification State refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.
 == bSync(none,none,none)==

@@ Line 29: / Line 29: @@
 This call forces backtracking after all b-threads reach the next state and after its badness is determined.
-== setBThreadEpsilon(double) ==
+== setBThreadEpsilon(<double epsilon>) ==
-This call defines non-determinism between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "Epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of non-deterministic execution, backtracking and exploration of alternative execution paths.
+This call defines non-determinism between b-threads. By default all b-threads are strictly ordered according to distinct priorities. If this call is used to set the "epsilon" to a value greater than zero, any two b-threads whose priorities differ by less than this value, are considered to be of the same priority, for the purpose of non-deterministic execution, backtracking and exploration of alternative execution paths.

← Older revision	Revision as of 09:42, 19 March 2014
(No difference)

@@ Line 8: / Line 8: @@
 == bSync(none,none,none)==
 While in regular runs a b-thread can terminate, in a model-checking run a b-thread should not terminate. You should precede or replace the return from runBthread method with a call to bSync(none,none,none). In a regular run this call will cause normal terminatation of the b-thread but in a model checking run it will suspend the b-thread in a state prior to terminating and allow backtracking from this state.
 == labelNextVerificationState(<label>)==
 This API calls provides a label for the next b-thread state and indirectly to the next composite system state.
@@ Line 16: / Line 17: @@
 * If a b-thread does not label its states – it is considered to have one state – and it does not increase the size of the Cartesian product. E.g. a b-thread that only counts events theoretically has infinitely many states. However, if this b-thread is known to never request or block events, it cannot affect the application flow, and if the counts do not matter in the counterexamples, there is no need to keep track of its exact state during back tracking.
 * A b-thread that incorrectly gives the same label to different states, may cause incorrect model-checking results.
 * Meaningful state names can help in debugging, but since since most b-threads are simple this is not critical. E.g., the states of a "linear" b-thread can be just numbered as 1/2/3 etc. The states of a b-thread can be labeled also based on the values of the variables that determine the state change.
 * State names are local to the b-thread and must be unique only within a b-thread. The BPmc infrastructure properly distinguishes state 1 of b-thread BT1, from state 1 of b-thread BT2.
@@ Line 27: / Line 28: @@
 == pruneAtNextVerificationState()==
 This call forces backtracking after all b-threads reach the next state and after its badness is determined.