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 | + | == Introduction == |
| − | * The BPmc model checker executes all possible paths of | + | * 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) | * BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | ||
| + | |||
| + | == Additional Information == | ||
| + | * [[BPmcAPI | BPmc API: Controlling the verification]] | ||
* [[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 | ||
| − | |||
Revision as of 10:45, 16 January 2014
Model Checking Behavioral Applications 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)
