Difference between revisions of "BPJ Model Checking"
From BP Wiki
| Line 4: | Line 4: | ||
* The BPmc model checker executes all possible paths of your program looking for states with desired and undesired properties per your specification. | * The BPmc model checker executes all possible paths of your 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) | ||
| − | * | + | * [[Nondetermism | Nondeterministic execution in behavioral programming]] |
* State awareness | * State awareness | ||
* Application Assistance | * Application Assistance | ||
| − | |||
Revision as of 13:59, 4 August 2013
Model Checking Behavioral Applications with BPmc
- You can find bugs and underspecification in behavioral programs using model checking.
- The BPmc model checker executes all possible paths of your 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)
- Nondeterministic execution in behavioral programming
- State awareness
- Application Assistance
