Difference between revisions of "BPJ Model Checking"
From BP Wiki
m (BPMC moved to BPJ Model Checking) |
(→Introduction) |
||
| Line 3: | Line 3: | ||
== Introduction == | == Introduction == | ||
* You can find bugs and under-specification in behavioral programs using model checking. | * You can find bugs and under-specification in behavioral programs using model checking. | ||
| − | * The model checking capability of BP (abbr. BPmc) is part of the overall | + | * The model checking capability of BP (abbr. BPmc) is part of the overall BPJ execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool. |
* During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification. | * During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification. | ||
* The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | * The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions) | ||
Revision as of 09:34, 19 March 2014
Verifying programs with BP model checking
Introduction
- You can find bugs and under-specification in behavioral programs using model checking.
- The model checking capability of BP (abbr. BPmc) is part of the overall BPJ execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
- During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
- The model checking capabilities support checking for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
- An application must be first enabled for model checking.
