Difference between revisions of "BPJ Model Checking API"
From BP Wiki
(New page: = BPmc API: Controlling model checking from your application = B-threads can call the following API methods *ToDo - of which object to control the model checking. * markNextVerificatio...) |
|||
| Line 1: | Line 1: | ||
= BPmc API: Controlling model checking from your application = | = BPmc API: Controlling model checking from your application = | ||
| − | B-threads can call the following API methods | + | B-threads can call the following API methods |
*ToDo - of which object | *ToDo - of which object | ||
to control the model checking. | to control the model checking. | ||
| − | * 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. | + | * 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. |
| − | * markNextVerificationStateAsHot(): This is 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. | + | * labelNextVerificationState(<label>): Provides a label for a b-thread state. It is the programmer's responsbility 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 b-thread doesn’t 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 counter examples, there is no need to keep track of its exact state during back tracking. |
| − | * 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. | + | * 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. |
| − | pruneAtNextVerificationState() | + | * markNextVerificationStateAsHot(): This is 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(): forces backtracking after all b-threads reach the next state and after its badness is determined. | |
| − | + | ||
| − | + | ||
Revision as of 05:33, 16 January 2014
BPmc API: Controlling model checking from your application
B-threads can call the following API methods
- ToDo - of which object
to control the model checking.
- 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>): Provides a label for a b-thread state. It is the programmer's responsbility 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 b-thread doesn’t 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 counter examples, there is no need to keep track of its exact state during back tracking.
- 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 is 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(): forces backtracking after all b-threads reach the next state and after its badness is determined.
