Verification of clocked and hybrid systems |
| |
Authors: | Yonit Kesten Zohar Manna Amir Pnueli |
| |
Affiliation: | (1) Department of Communication Systems Engineering, Ben Gurion University, Beer-Sheva, Israel (e-mail: ykesten@bgumail.bgu.ac.il), IL;(2) Department of Computer Science, Stanford University, Stanford, CA 94305, USA (e-mail: manna@cs.stanford.edu), US;(3) Department of Computer Science, Weizmann Institute, Rehovot, Israel (e-mail: amir@wisdom.weizmann.ac.il), IL |
| |
Abstract: | This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed 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 of response properties 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 given CTS isnon-zeno.
Finally, we present an extension of the model and the invariance proof rule for hybrid systems.
Received: 23 September 1998 / 7 June 1999 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|