Timed Weak Simulation Verification and Its Application to Stepwise Refinement of Real-Time Software