Verification of clocked and hybrid systems
Verification of clocked and hybrid systems
复制标题
DOI：
10.1007/s002360050177
复制
发表时间：
1996-11
期刊：
影响因子：
0.6
通讯作者：
Y. Kesten;Z. Manna;A. Pnueli
中科院分区：
文献类型：
--
作者：
Y. Kesten;Z. Manna;A. Pnueli
本文提出了一种新的实时系统计算模型--锁定变迁系统（CTS）模型。CTS模型是我们以前的过渡模型的发展，其中一些变化是受到时间自动机模型的启发。新的模型导致一个更简单的风格的时间规范和验证，不需要扩展的时间语言。我们提出的验证规则，证明安全性和活性的时钟转换系统的属性。所有规则都与验证图相关联。响应属性的验证需要调整的证明规则开发的不定时系统，反映了这样一个事实，即在真实的时间系统的进展是由时间的进展，而不是由公平性。验证规则的风格是非常接近的验证风格的untimed系统，它允许（再）使用的验证方法和工具，开发的untimed反应式系统，证明所有有趣的性质的实时系统。我们提出了一个扩展的模型和不变性证明规则的混合系统。
This paper presents a new computational model for real-time systems, called theclocked transition system(CTS) model. TheCTSmodel is a development of our previoustimed transitionmodel, where some of the changes are inspired by the model oftimed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety a nd liveness properties of clocked transition systems. All rules are associated with verification diagrams. The verification ofresponseproperties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for u ntimed reactive systems, for proving all interesting properties of real-time systems.We conclude with the presentation of a branching-time based approach for verifying that an arbitrary givenCTSisnon-zeno.Finally, we present an extension of the model and the invariance proof rule for hybrid systems.