Difference between revisions of "BPJ Model Checking"
From BP Wiki
| Line 6: | Line 6: | ||
* [[Nondetermism | Nondeterministic execution in behavioral programming]] | * [[Nondetermism | Nondeterministic execution in behavioral programming]] | ||
* [[RunMode | Run mode specification for model-checking]] | * [[RunMode | Run mode specification for model-checking]] | ||
| − | * [[BPmc Parameteres | BPmc execution parameters]] | + | * [[BPmc Parameteres | BPmc execution parameters]] |
* State awareness | * State awareness | ||
| − | * Application Assistance | + | * [[BPmcAPI | Application Assistance]] |
Revision as of 05:16, 16 January 2014
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
- Run mode specification for model-checking
- BPmc execution parameters
- State awareness
- Application Assistance
