Uninterrupted Automatic Broadcasting Based on Timed Automata

This paper analyzes the system demand ofuninterrupted automatic broadcasting of radio station, conducts research on the protocol mechanism and operational principle, and proposes a primary-backup synchronization and switching mechanism based on the network. In order to ensure the correctness and safety of this mechanism, we established the timed automata based model for primary playout station, backup playout station, communication network and failures. The protocol sequence diagrams simulated in UPPAAL shows thecorrectness of the protocol design. Furthermore, the reachability, safety, liveness and other formulas are checked through model checking in the verifier. The results indicate the mechanism designed in this paper is safe and reliable.