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...) |
|||
| Line 1: | Line 1: | ||
= Model Checking Behavioral Applications with BPmc | = Model Checking Behavioral Applications with BPmc | ||
| − | You can find bugs and underspecification in behavioral programs using model checking. | + | You can find bugs and underspecification in behavioral programs using model checking. |
| − | The BPmc model checker executes all possible paths of your program looking for states with desired and undesired properties per | + | The BPmc model checker executes all possible paths of your program looking for states with desired and undesired properties per |
your specification. | your specification. | ||
| − | * [Nondetermism | Nondeterminisim in behavioral programming]] | + | * [[Nondetermism | Nondeterminisim in behavioral programming]] |
Revision as of 13:33, 4 August 2013
= 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 paths of your program looking for states with desired and undesired properties per your specification.
