Performance Evaluation : = (Process Algebra + Model Checking) × Markov Chains