Difference between revisions of "BPJ Model Checking"

From BP Wiki
Jump to: navigation, search
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.
 +
* BPmc can check for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)
 +
* Backtracking
 +
* State awareness
 +
* Application Assistance
 
* [[Nondetermism | Nondeterminisim in behavioral programming]]
 
* [[Nondetermism | Nondeterminisim in behavioral programming]]

Revision as of 13:56, 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.

  • BPmc can check for safety properties (including deadlocks) and for liveness properties (with fairness assumptions)
  • Backtracking
  • State awareness
  • Application Assistance
  • Nondeterminisim in behavioral programming