BPJ Model Checking

From BP Wiki
Revision as of 13:56, 4 August 2013 by Assaf (Talk | contribs)

Jump to: navigation, search

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
Retrieved from "https://wiki.weizmann.ac.il/bp/index.php?title=BPJ_Model_Checking&oldid=40"