Difference between revisions of "BPJ Model Checking"
From BP Wiki
(New page: = 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 path...) |
(→Introduction) |
||
| (31 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
| − | = | + | = Verifying programs with BP model checking = |
| − | You can find bugs and | + | == Introduction == |
| − | The BPmc model | + | * You can find bugs and under-specification in behavioral programs using model checking. |
| − | your specification. | + | * 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. |
| − | * [Nondetermism | | + | * 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. | ||
| + | * Verification Example: [http://www.wisdom.weizmann.ac.il/~bprogram/videos/TTTVerification.avi Movie: Using model-checking to repair a behavioral program for play Tic Tac Toe]: | ||
| + | ** We present a program for playing Tic Tac Toe and verify it using BP model checking. | ||
| + | ** When the b-thread for adding the third O in a line is removed, the program may lose the game. | ||
| + | ** "coding" and adding the b-thread, causes the program to never lose the game. | ||
| + | |||
| + | == Additional Information == | ||
| + | * [[BPJ Model Checking API| BPJ Model Checking API: Enabling your application for model-checking and controlling its verification]] | ||
| + | * [[RunMode | Run modes and execution parameters for model-checking]] | ||
| + | * [[Nondetermism | Nondeterministic execution in behavioral programming]] | ||
| + | * [[JavaFlow | More information about enabling your application for model-checking]] | ||
Latest revision as of 19:20, 27 April 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.
- Verification Example: Movie: Using model-checking to repair a behavioral program for play Tic Tac Toe:
- We present a program for playing Tic Tac Toe and verify it using BP model checking.
- When the b-thread for adding the third O in a line is removed, the program may lose the game.
- "coding" and adding the b-thread, causes the program to never lose the game.
