Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Procotol