Revision as of 12:40, 11 February 2014

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.

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 BPmc 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.

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.

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.

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.