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

• BPmc API: Controlling model checking from your application
• Run modes and execution parameters for model-checking
• Nondeterministic execution in behavioral programming
• State awareness
• BPmc Internals: BPmc and the *javaflow* package