S. Abdi and D. Gajski, "Provably Correct Architecture Refinement," TR 03-29, September 30, 2003. download pdf