\section{Introduction}

A formal framework for specifying and verifying temporal properties of
reactive systems often contains the following components:
\begin{itemize}
\item A \emm{computational model} defining the set of behaviors
(computations) that are to be associated with systems in the
considered model.
\item A \emm{requirement specification} language for specifying
properties of systems within the model. The languages we have
considered in our previous work are all variants of temporal logic
extended to deal with various aspects specific to the considered
model, such as real-time and continuously changing variables.
\item A \emm{system description} language for describing systems
within the model. We frequently use both a textual programming language and
appropriate extensions of the graphical language of statecharts
\cite{H} to present systems.
\item A set of \emm{proof rules} by which valid properties of systems
can be verified, showing that the systems satisfy their specifications.
\item A set of \emm{algorithmic methods} enabling a fully automatic
verification of decidable subclasses of the verification problem such
as the verification of finite-state systems (\emm{model checking}).
\end{itemize}

\nin
In \cite{ModR}, we considered a hierarchy of three models, each
extending its predecessor, as follows:
\begin{itemize}
\item A \emm{reactive systems} model that captures the
\emm{qualitative} (non-quantitative) temporal precedence
aspect of time. This model can only identify that one event precedes
another but not by how much.
\item A \emm{real-time systems} model that captures the \emm{metric}
aspect of time in a reactive system. This model can measure the time
elapsing between two events.
\item A \emm{hybrid systems} model that allows the inclusion of
\emm{continuous} components in a reactive real-time system. Such
continuous components may cause continuous change in the values of
some state variables according to some physical or control law.
\end{itemize}

\nin
The computational model proposed for reactive systems is that of a
\emm{fair transition system} (\fts) \cite{MPB}.

The approach to real time presented in \cite{ModR} and
\cite{TPMTTS} is based on the computational model of \emm{timed
transition systems} (\ttss) in which time itself is not explicitly
represented but is reflected in a time stamp affixed to each state in
a computation of a \ttss. As a result of time not being available as a
value of some variable, the requirement specification language must be
based on a necessary extension of temporal logic. In \cite{ModR}, we
present two such extensions: \emm{metric temporal logic} (\mtl) which
introduces bounded versions of the temporal operators, subscripted by
an interval specification, and \emm{temporal logic with age} (\tlg)
which introduces the operator $\Gamma$, measuring the length of recent
time in which a certain formula held continuously.

Consider, for example, the following important timed properties:
\begin{itemize}
\item \emm{Bounded response}:\quad Every $p$ should be followed by an
occurrence of a $q$, not later than $d$ time units.
\item \emm{Minimal separation}:\quad No $q$ can occur earlier than $d$
time units after an occurrence of $p$.
\end{itemize}

\nin
In \mtl, these two properties can be specified as follows:
\[\begin{array}{lll}
\bullet & \mbox{\rm Bounded response:}   & p\ \ent\ \F_{\leq d}\ q.\\[4pt]
\bullet & \mbox{\rm Minimal separation:}\quad & p\ \ent\ \G_{<d}\,\neg q.
\end{array}
\]

This approach to the specification of timing properties has been
advocated in \cite{KVdR}, \cite{KdR}, and \cite{Koy90}, although an
early proposal in \cite{BH81} can be viewed as a precursor to this
specification style.

\nin
Using \tlg, the same properties can be specified by:
\[\begin{array}{lll}
\bullet & \mbox{\rm Bounded response:}   & \G\Bigl[\Gamma\Bigl((\neg q) \since
(p\wedge\neg q)\Bigr)\ \leq\ d\Bigr].\\[4pt]
\bullet & \mbox{\rm Minimal separation:}\quad & q\quad \ent \quad
\Bigl(\opH(\neg p)\;\vee\;\Gamma(\neg p)\geq d\Bigr). 
\end{array}
\]
When constructing detailed proofs of such timed properties, we found
it necessary to form many auxiliary invariants involving the age
function $\Gamma$. Very soon, we realized that each age expression of
the form $\Gamma(p)$ represents a timer that started measuring time as
soon as $p$ becomes true and is reset (or shut off) whenever $p$
becomes false. This led to the suggestion that age expressions can be
eliminated in favor of the introduction of explicit timers.

Meanwhile, the model of timed automata \cite{AD94} has gained
dominance in the arena of real-time algorithmic verification. This
model uses timers which can only be reset by system transitions but
increase uniformly whenever time progresses. However, aiming at
algorithmic verification, this model can only capture finite-state
systems.

In this paper we present a new computational model for real-time
systems: \emm{clocked transition system} (\ctss). This model
represents time by a set of clocks (timers) which increase uniformly
whenever time progresses, but can be set to arbitrary values by system
(program) transitions.

It is easy and natural to stipulate that one of the clocks $T$ is never
reset. In this case, $T$ represents the \emm{master clock} measuring
real time from the beginning of the computation. This immediately
yields the possibility of specifying timing properties of systems by
unextended temporal logic, which may refer to any of the system
variables, including the master clock $T$. Thus, the two yardstick
properties considered above can be specified by the following
(unextended) temporal formulas:
\[\begin{array}{lll}
\bullet & \mbox{\rm Bounded response:}   & p\;\land\; (T=t_0)\quad \ent\quad
\F(q\;\land\; T\leq t_0+d).\\[4pt]
\bullet & \mbox{\rm Minimal separation:}\quad & p\;\land\;
(T=t_0)\quad \ent\quad \G(T<t_0+d\;\to\;\neg q). 
\end{array}
\]

\nin A first advantage of the new computational model over its
predecessors is that it leads to a more natural style of verification
proofs, stating invariants in terms of clocks, which are just another
kind of system variables, instead of formulating invariants in terms
of $\Gamma$-expressions. A second advantage is that we can use
temporal logic without any extensions as the specification language, and
can reuse many of the methods and tools developed for verifying
reactive systems, under the \fts\ computational model, for verifying
real-time systems under the \ctss\ model. Another advantage of the
\ctss\ model is that it can be viewed as a natural first-order
extension of the timed automata model \cite{AD94}.

In order to reuse \fts\ verification methods for verifying \ctss\
properties, we will show that for every \ctss\ $\Phi$ there exists a
corresponding \fts\ $P_{\Phi}$ such that the runs of $\Phi$ and the
runs of $P_{\Phi}$ coincide. It follows that any safety property is
valid over the \ctss\ $\Phi$ iff it is valid over the \fts\
$P_{\Phi}$. This reduction from real-time systems to simpler
transition systems enables us to use the deductive methodology
developed for proving safety properties of reactive systems, as well
as support systems for this methodology such as \cite{STeP}, for
establishing safety properties of timed systems.

It is interesting to note that the move from \ttss\ to \ctss\ brings
us closer to the approach proposed in \cite{AL91}, which also
recommends handling real time with a minimal extension of the
reactive-systems formalism.

The restriction to safety properties is not as constraining as one may
think. Many properties whose untimed version falls into the liveness
class become safety properties when we consider their timed version.
For example, termination of a program is a liveness property. However,
the property of termination within 15 time units is a safety property.
This indicates that, when we move to real-time systems, the set of
safety properties we may want to prove constitutes an even higher
portion of the total set of properties of interest than in the case of
untimed reactive-systems. We refer the reader to \cite{IPL} and
\cite{vital} for further discussions of this point.

We refer the reader to
\marginpar{\em refer to the two Henzinger's papers}
\cite{TPTL1}, \cite{BOST}, \cite{AL91}, and the
survey in \cite{AHsur}, for additional logics, models, and approaches
to the verification of real-time systems. In the process algebra
school, some of the representative approaches to real time are
\cite{NSY91}, \cite{MT90}, and many others are listed in \cite{Si91}.

The paper is organized as follows. In Section~\ref{cts}, we present
the real-time computational model of \emm{clocked transition systems}
(\ctss). In Section~\ref{programs}, we show how programs augmented
with timing bounds for the execution of statements can be represented
as clocked transition systems. In Section~\ref{safety}, we present
rules and verification diagrams for verifying safety properties of
\ctss's. In Section~\ref{response}, we present rules and verification
diagrams for establishing response properties of clocked transition
systems. Finally, in Section~\ref{nonzenos}, we present an approach to
verifying that a given \ctss\ is non-zeno.


