(Created page with 'Category:User Manual') |
No edit summary |
||
| Line 1: | Line 1: | ||
[[Category:User Manual]] | [[Category:User Manual]] | ||
ProB also offers an alternative checking method, inspired by the Alloy | |||
<ref>D. Jackson: Alloy: A lightweight object modelling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion), independently of the particular initialisation of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding). | |||
Warning: this feature of ProB has not received the same level of attention and testing as animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, hence it will probably only work for simpler B machines. | |||
=Difference between Constraint Based Checking and Model Checking= | |||
Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property, but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules. | |||
=Commands of the Constraint Based Checker = | |||
These commands are only accessible in the Normal mode of ProB (see [[General Presentation (tcl/tk)#The ProB main window|General Presentation]]) and are in the submenu Verify|Constraint Based Checking. The command Constraint Search for Invariant Violations will execute the constraint based checking described above, checking for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command Constraint Search for Invariant Violations... enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking. | |||
The Constraint Search for Assertion Violations command executes the constraint based checking looking for assertion violations, while the command Constraint Search for Abort Conditions executes it looking for abort conditions. | |||
=References= | |||
<references /> | |||
ProB also offers an alternative checking method, inspired by the Alloy
[1] analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion), independently of the particular initialisation of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).
Warning: this feature of ProB has not received the same level of attention and testing as animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, hence it will probably only work for simpler B machines.
Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property, but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.
These commands are only accessible in the Normal mode of ProB (see General Presentation) and are in the submenu Verify|Constraint Based Checking. The command Constraint Search for Invariant Violations will execute the constraint based checking described above, checking for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command Constraint Search for Invariant Violations... enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.
The Constraint Search for Assertion Violations command executes the constraint based checking looking for assertion violations, while the command Constraint Search for Abort Conditions executes it looking for abort conditions.