BPJ Model Checking

From BP Wiki
Revision as of 13:40, 11 February 2014 by Assaf (Talk | contribs)

Jump to: navigation, search

Verifying programs 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)
  • An application must be first enabled for model checking.

Additional Information