BPJ Model Checking - Revision history

Assaf: /* Introduction */

2014-04-27T19:20:08Z

‎Introduction

2014-04-27T19:17:07Z

‎Introduction

2014-03-19T09:43:13Z

‎Additional Information

2014-03-19T09:34:55Z

‎Introduction

2014-03-19T09:33:30Z

2014-02-12T09:23:10Z

‎Introduction

2014-02-12T09:22:47Z

‎Introduction

2014-02-12T09:20:27Z

2014-02-11T13:41:22Z

‎Additional Information

2014-02-11T13:40:51Z

‎Additional Information

@@ Line 7: / Line 7: @@
 * The model checking capabilities support checking for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)
 * An application must be first enabled for model checking.
-* Verification Example: [http://www.wisdom.weizmann.ac.il/~bprogram/videos/TTTVerification.avi  Movie: Using model-checking to repair a behavioral program for play Tic Tac Toe]
+* Verification Example: [http://www.wisdom.weizmann.ac.il/~bprogram/videos/TTTVerification.avi  Movie: Using model-checking to repair a behavioral program for play Tic Tac Toe]:
 == Additional Information ==

@@ Line 7: / Line 7: @@
 * The model checking capabilities support checking for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)
 * An application must be first enabled for model checking.
 == Additional Information ==

@@ Line 9: / Line 9: @@
 == Additional Information ==
-* [[BPmcAPI | BPmc API: Enabling your application for model-checking and controlling its verification]]
+* [[BPJ Model Checking API| BPJ Model Checking API: Enabling your application for model-checking and controlling its verification]]
 * [[RunMode | Run modes and execution parameters for model-checking]]
 * [[Nondetermism | Nondeterministic execution in behavioral programming]]
 * [[JavaFlow | More information about enabling your application for model-checking]]

@@ Line 3: / Line 3: @@
 == Introduction ==
 * You can find bugs and under-specification in behavioral programs using model checking.
-* The model checking capability of BP (abbr. BPmc) is part of the overall BP execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
+* The model checking capability of BP (abbr. BPmc) is part of the overall BPJ execution infrastructure. Thus, the program can be verified directly by executing it (with appropriate setup) subject to all relevant alternatives. There is no need to create a separate model or abstraction to be verified by an external tool.
 * During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
 * The model checking capabilities support checking for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)

@@ Line 6: / Line 6: @@
 * During model checking execution, the BP infrastructure executes all possible paths of a behavioral program looking for states with desired and undesired properties per your specification.
 * The model checking capabilities support checking for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)
-* [[BPmcAPI#pruneSearchNow.28.29 | An application must be first enabled for model checking]].
+* An application must be first enabled for model checking.
 == Additional Information ==

← Older revision	Revision as of 09:33, 19 March 2014
(No difference)