  Traditionally, practitioners use formal methods pre-dominately for one half
of the quality-assurance process: verification (do we build the software
right?). The other half -- validation (do we build the right software?) -- has
been given comparatively little attention. While verification is the core of
refinement-based formal methods, where each new refinement step must preserve
all properties of its abstract model, validation is usually postponed until the
latest stages of the development, when models can be automatically executed.
Thus mistakes in requirements or in their interpretation are caught too late:
usually at the end of the development process. In this paper, we present a
novel approach to check compliance between requirements and their formal
refinement-based specification during the earlier stages of development. Our
proposed approach -- "validation obligations" -- is based on the simple idea
that both verification and validation are an integral part of all refinement
steps of a system.
