This paper presents a new computational model for realtime 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 and
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 untimed
reactive systems, for proving all interesting properties of realtime
systems.
We conclude with the presentation of a branchingtime based approach
for verifying that an arbitrary given CTS is nonzeno.
Finally, we present an extension of the model and the invariance proof
rule for hybrid systems.
Acta Informatica