Robust Model-Checking of Linear-Time Properties in Timed Automata
Robust Model-Checking of Linear-Time Properties in Timed Automata
复制标题
定时自动机中线性时间特性的鲁棒模型检查
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Pierre
中科院分区：
文献类型：
--
作者：
P. Bouyer;N. Markey;Pierre
时间系统的形式化验证已经很好地理解了，但是它们的实现仍然具有挑战性。Raskin等人最近提出了一个参数化时间自动机模型，其中过渡可能会稍微延迟或加速。这个模型被用来证明一个定时系统是可实现的安全属性，通过证明参数化模型鲁棒地满足安全属性。我们在这里扩展的概念，可实现性更广泛的类的线性时间属性，并提供PSPSACE算法的强大的模型检查布奇和LTL属性。我们还展示了如何调整这些算法，以验证有界响应时间属性。
Formal verification of timed systems is well understood, but their implementation is still challenging. Raskin et al. have recently brought out a model of parameterized timed automata in which the transitions might be slightly delayed or expedited. This model is used to prove that a timed system is implementable with respect to a safety property, by proving that the parameterized model robustly satisfies the safety property. We extend here the notion of implementability to the broader class of linear-time properties, and provide PSPSACE algorithms for the robust model-checking of Buchi-like and LTL properties. We also show how those algorithms can be adapted in order to verify bounded-response-time properties.