BPJ Model Checking 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.
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 Next Verification State refers to the applictation's (composite) state at next synchronization point, when all b-threads are synchronized.
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.
- 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 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 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. 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 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.
pruneAtNextVerificationState()
This call forces backtracking after all b-threads reach the next state and after its badness is determined.
setBThreadEpsilon(<double epsilon>)
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.
