(Created page with '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 ch…') |
|||
| Line 7: | Line 7: | ||
=How does it work?= | =How does it work?= | ||
# | # 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. | ||
# | # 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. | ||
ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines.
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.