一种唇同步协议的鲁棒可达性再验证
Re-verification of a Lip Synchronization Protocol using Robust Reachability
摘要：
时间自动机是描述和分析实时系统的重要模型。鲁棒性是在时钟出现小漂移或测试防护装置不精确的情况下模型的正确性。实现了一种分析时间自动机鲁棒性的符号算法。在本文中，我们重新分析了一个工业案例唇同步协议使用新的鲁棒可达性算法。这个唇同步协议是一个有趣的情况下，因为定时方面是至关重要的协议的正确性。该模型的几个版本被认为是：一个理想的视频流，锚定抖动，和非锚定抖动。
英文摘要：
The timed automata formalism is an important model for specifying and analysing real-time systems. Robustness is the correctness of the model in the presence of small drifts on clocks or imprecision in testing guards. A symbolic algorithm for the analysis of the robustness of timed automata has been implemented. In this paper, we re-analyse an industrial case lip synchronization protocol using the new robust reachability algorithm. This lip synchronization protocol is an interesting case because timing aspects are crucial for the correctness of the protocol. Several versions of the model are considered: with an ideal video stream, with anchored jitter, and with non-anchored jitter.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
