Total Correctness Type Refinements for Communicating Processes