Verification, Performance Analysis and Controller Synthesis for Real-Time Systems