Formal Design and Verification of Dynamic Caching for Automatic Playout System

This paper analyzes the key technology of uninterrupted broadcast, describes the working principle and processes of the dynamic caching scheme. After extracting the features and needs, this paper adopts the UPPAAL based on timed automata theory to construct the model, and describes the expected properties by using TCTL language, and then performs automatic verification based on model checking. Eventually, we complete the design which conforms to requirements and passes validation by observing the simulated trace, analyzing counter examples, and modifying model repeatedly. Through formal modeling and model checking, we reduce design errors, avoid some system faults which are generated during development and running phase, and improve the reliability and safety of the system. All of the above lay a good foundation for the design and implementation of the playout system.