Difference between revisions of "BPJ Model Checking"
From BP Wiki
(→Additional Information) |
|||
| Line 10: | Line 10: | ||
* [[RunMode | Run modes and execution parameters for model-checking]] | * [[RunMode | Run modes and execution parameters for model-checking]] | ||
* [[Nondetermism | Nondeterministic execution in behavioral programming]] | * [[Nondetermism | Nondeterministic execution in behavioral programming]] | ||
| − | |||
* [[JavaFlow | Enabling your application for model-checking]] | * [[JavaFlow | Enabling your application for model-checking]] | ||
Revision as of 13:39, 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)
