I. Introduction
The task of verifying an implementation against its functional specification is influenced by the choice of the models used, as well as by the design methodology. This paper shows how transaction-based models can be advantageous in the context of refinement checking.