Difference between revisions of "BPJ Model Checking"
From BP Wiki
(→Additional Information) |
(→Introduction) |
||
| Line 5: | Line 5: | ||
* The BPmc model checker executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification. | * The BPmc model checker executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification. | ||
* BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | * BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | ||
| + | * An application must be first enabled for model checking. | ||
== Additional Information == | == Additional Information == | ||
Revision as of 13:40, 11 February 2014
Verifying programs with BPmc
Introduction
- You can find bugs and under-specification in behavioral programs using model checking.
- The BPmc model checker executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
- BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
- An application must be first enabled for model checking.
