Refinement Checking: Difference between revisions
No edit summary |
(Update wiki link) |
||
| (3 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
[[Category:User Manual | [[Category:User Manual]] | ||
[[Category:Stubs]] | |||
{{Revision}} | {{Revision}} | ||
ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines. | ProB can be used for refinement checking of B, Z and CSP specifications. Below we first discuss refinement checking for B machines. | ||
There is a tutorial on checking CSP assertions in ProB which can be viewed [[Checking CSP Assertions|here]]. | |||
=What kind of refinement is checked?= | =What kind of refinement is checked?= | ||
| Line 10: | Line 12: | ||
# 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. | ||
Latest revision as of 17:23, 4 February 2021
|
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. There is a tutorial on checking CSP assertions in ProB which can be viewed here.
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?
- 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.