The Surprising Robustness of (Closed) Timed Automata against Clock-Drift
The Surprising Robustness of (Closed) Timed Automata against Clock-Drift
复制标题
（封闭）定时自动机对时钟漂移的惊人鲁棒性
DOI：
10.1007/978-0-387-09680-3_36
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
J.-P. Katoen
中科院分区：
文献类型：
--
作者：
M. Swaminathan;M. Fränzle;J.-P. Katoen
我们在“鲁棒性”的概念下研究了作为时间自动机（TA）建模的时间系统的可达性（或等效的安全性），即当TA的时钟可能漂移少量时。我们的贡献有两个方面：(1)我们首先考虑了Puri[1]引入的时钟漂移模型，随后在其他作品中进行了研究[2,3,4]。我们表明，当测试具有任意但有限生命周期的定时系统的鲁棒安全性时，由诸如UPPAAL之类的工具执行的基于标准区域的前向可达性分析实际上是精确的具有封闭保护、不变量和目标的TA。(2)接下来，我们考虑了一个更现实的漂移时钟模型，该模型考虑了大多数实际系统中执行的规则再同步。然后，我们展示了像UPPAAL这样的工具的标准可达性分析再次足以测试时钟漂移模型中的鲁棒安全性，对于具有封闭保护、不变量和目标的TA，但是现在对系统生命周期没有任何限制。
We investigate reachability (or equivalently, safety) for timed systems modelled as Timed Automata (TA) under notions of “robustness”, i.e., when the clocks of the TA may drift by small amounts. Our contributions are two-fold: (1) We first consider the model of clock-drift introduced by Puri [1] and subsequently studied in other works [2,3,4]. We show that the standard zone-based forward reachability analysis performed by tools such as UPPAAL is in fact exact for TA with closed guards, invariants, and targets, when testing robust safety of timed systems having an arbitrary, but finite lifetime. (2) Next, we consider a more realistic model of drifting clocks that takes into account the regular resynchronization performed in most practical systems. We then show that the standard reachability analysis of tools like UPPAAL again suffices to test for robust safety in this model of clock-drift, for TA with closed guards, invariants, and targets, but now without any restrictions on system life-time.
登录
查看更多内容
定时自动机的鲁棒性和可实现性
DOI：
--
发表时间：
2004
期刊：
FORMATS/FTRTFT
影响因子：
--
作者：
M. Wulf;L. Doyen;N. Markey;Jean
通讯作者：
Jean
鲁棒定时自动机
影响因子：
--
作者：
Vineet Gupta;T. Henzinger;R. Jagadeesan
通讯作者：
R. Jagadeesan
重新审视定时自动机的数字化、鲁棒性和可判定性
DOI：
--
发表时间：
2003
期刊：
18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings.
影响因子：
--
作者：
Joël Ouaknine;J. Worrell
通讯作者：
J. Worrell
定时自动机中线性时间特性的鲁棒模型检查
DOI：
--
发表时间：
2006
期刊：
Latin American Symposium on Theoretical Informatics
影响因子：
--
作者：
P. Bouyer;N. Markey;Pierre
通讯作者：
Pierre
通过通道机进行定时自动机的鲁棒分析
DOI：
--
发表时间：
2008
期刊：
Foundations of Software Science and Computation Structure
影响因子：
--
作者：
P. Bouyer;N. Markey;Pierre
通讯作者：
Pierre