Difference between revisions of "BPJ Model Checking"
From BP Wiki
| Line 1: | Line 1: | ||
= Model Checking Behavioral Applications with BPmc= | = Model Checking Behavioral Applications with BPmc= | ||
| − | You can find bugs and underspecification in behavioral programs using model checking. | + | * 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 | + | * The BPmc model checker executes all possible paths of your program looking for states with desired and undesired properties per |
your specification. | your specification. | ||
| + | * BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | ||
| + | * Backtracking | ||
| + | * State awareness | ||
| + | * Application Assistance | ||
* [[Nondetermism | Nondeterminisim in behavioral programming]] | * [[Nondetermism | Nondeterminisim in behavioral programming]] | ||
Revision as of 13:56, 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)
- Backtracking
- State awareness
- Application Assistance
- Nondeterminisim in behavioral programming
