Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method