Difference between revisions of "BPJ Model Checking"

From BP Wiki
Jump to: navigation, search
Line 11: Line 11:
 
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
 
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
 
* State awareness
 
* State awareness
* [[JavaFlow | BPmc Internals: BPmc and the *javaflow* package]]
+
* [[JavaFlow | BPmc Internals: BPmc and the Javaflow package]]

Revision as of 11:33, 16 January 2014

Model Checking Behavioral Applications 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)

Additional Information