The most effective way to decompose the specification and verification of a system into manageable parts is to define an abstract model as a specification, and then to specify ``refinement maps'' that relate abstract model behaviors to implementation behaviors. Generally, abstract models specify ``what'' is being done, without specifying the ``how'', ``where'' or ``when''. The ``where'' and ``when'' are given by the refinement maps, while the implementation determines the ``how''. In the simplest case the abstract model does nothing at all. For example, in the case of a link-layer protocol that simply transfers a stream of data from point A to point B without modifying it, there is no ``what'' and the only important information is the ``where'' and ``when''. The abstract model in this case might consist only of the stream of data itself. In the case of a microprocessor, the abstract model might determine the sequence of instructions that are executed according to the ISA (instruction set architecture). The refinement map would determine what instruction appears at each stage of the pipeline at any given time.