Difference between revisions of "BPJ Model Checking"
From BP Wiki
| Line 1: | Line 1: | ||
| − | = | + | = Verifying programs with with BPmc= |
== Introduction == | == Introduction == | ||
| Line 11: | Line 11: | ||
* [[Nondetermism | Nondeterministic execution in behavioral programming]] | * [[Nondetermism | Nondeterministic execution in behavioral programming]] | ||
* State awareness | * State awareness | ||
| − | * [[JavaFlow | BPmc | + | * [[JavaFlow | Programming requirements for working with BPmc]] |
Revision as of 13:07, 16 January 2014
Verifying programs with 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)
