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.
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.