A Refinement Relation Supporting the Transition from Unbounded to Bounded Communication Buffers