A Protocol and Correctness Proofs for Real-Time High-Performance Broadcast Networks