Refinement Checking: Difference between revisions

No edit summary
m (" ")
Line 11: Line 11:


# Open the abstract specification, explore its state space (e.g.,using an exhaustive temporal model check).
# Open the abstract specification, explore its state space (e.g.,using an exhaustive temporal model check).
# Use the command "Save state for later refinement check" in the Verify menu.
# Use the command "Save state for later refinement check" in the "Verify" menu.
# Open the refinement machine.
# Open the refinement machine.
# You can now use the "Refinement Check..." command in the Verify menu.
# You can now use the "Refinement Check..." command in the "Verify" menu.

Revision as of 11:49, 18 April 2011

Out of date icon.png Warning This page has not yet been reviewed. Parts of it may no longer be up to date

ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines.

What kind of refinement is checked?

ProB checks trace refinement. In other words, it checks whether every trace (consisting of executed operations with their parameter values and return values) of a refinement machine can also be performed by the abstract specification.

Hence, ProB does *not* check the gluing invariant. Also, PRE-conditions are treated as SELECT and PRE-conditions of the abstract machine are *not* always propagated down to the refinement machine. Hence, refinement checking has to be used with care for classical B machines, but it is well suited for EventB-style machines.

How does it work?

  1. Open the abstract specification, explore its state space (e.g.,using an exhaustive temporal model check).
  2. Use the command "Save state for later refinement check" in the "Verify" menu.
  3. Open the refinement machine.
  4. You can now use the "Refinement Check..." command in the "Verify" menu.