Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures