Real-Time Model Checking of Embedded Systems