\section{Programs as Clocked Transition Systems}
\label{consb}
\label{programs}
In this section we show how to represent real-time programs as clocked
transition systems.

In \cite{MPB}, we introduced a simple programming language \spl. Here
we consider a subset of the language, restricting our attention to the
following statements:
\begin{quote}
\emm{skip, assignment, await, noncritical, critical, conditional,
concatenation, selection, while, \mbox{\rm and} block}.
\end{quote}
Not including the \emm{cooperation} statement has the effect that
parallelism is allowed only at the top level of the program. That is,
a program is a parallel copmposition of processes, each of which is
sequential.

We refer the reader to Chapter 0 of \cite{MPB2} for the construction
of a fair transition system $\Fsysp$ corresponding to an \spl\ program
$P$. This construction associates a single transition with each
\emm{executable} statement, which include all statements except
\emm{concatenation}, \emm{selection}, and \emm{block}.
Here, we deviate from the construction of \cite{MPB2} in the
transition associated with the \emm{await} statement. Instead, we
associate with each statement of the form
\[\lscr\colon\ \hbox{\bf await}\ c;\quad\wh{\lscr}\colon\]
a transition $\tau_{\lscr}$, whose transition relation $\rho_{\lscr}$
is given by
\[\rho_{\lscr}\colon\quad
\ell\in \pi \lwedge 
	\left(\begin{array}{l}
	\pos c\ \wedge\ \pi\pri=\pi-\{\ell\}\cup\{\wh{\ell}\} \\
		\quad\vee\\
	\neg c\ \wedge\ \pi\pri=\pi
\end{array}\right)\lwedge \pres(V-\{\pi\})
.\]
Otherwise than the \emm{await} statement, we follow \cite{MPB2} in the
association of transitions with executable statements.

Another difference from \cite{MPB2} is that we only associate
transitions with the executable statements  and do not add the idling
transition $\tauI$.

Let $P$ be an \spl\ program. To obtain a real-time program, we
associate with each $S$, an executable statement of $P$, a pair of
values $[\ls,\us]$, called the \emm{lower} and \emm{upper} bounds of
$S$. These values, satisfying $0\le \ls\le\us\le \infty$, are intended
to provide a lower and upper bound on the length of time the statement
can be enabled without being taken. We refer to a program with an
assignment of time bounds as an \splt\ program, and view it as a
real-time program.

Note that assigning time bounds to each executable statement of $P$ is
equivalent to assigning time bounds $[l_{\tau}, u_{\tau}]$ to each
transition $\tau$ associated with an executable statement.

\subsection{The \ctss\ corresponding to an \splt\ program}
Let $P$ be an \splt\ program. That is, an \spl\ program with
time bounds $[l_{\tau}, u_{\tau}]$ associated with each transition
$\tau\in\Tau_P-\{\tauI\}$. We will show how to construct a \ctss\
$\Phi_{P}$ corresponding to the \splt\ program $P$.

As a first step, we construct the \fts\ $\Fsysp\colon
\bigl<V,\Theta,\Tau,\cJ,\cC\bigr>$ corresponding to program $P$. Note
that if program $P$ uses only the statements in the previously
presented subset, then $\cJ = \Tau-\{\tauI\}$ and $\cC = \emptyset$.
Assume that program $P$ is a parallel composition of $m$ processes.
That is, $P$ has the form
\[\mbox{\rm declarations}; \quad P_1\ \pll\ \cdots\ \pll\ P_m,\]
where each $P_i$ is a (sequential) statement.

The \ctss\ corresponsing to $P$ is given by $\Phi_{P} \colon
\bigl<\wtV,\wtTheta,\wtTau,\Pi\bigr>$, where
\begin{itemize}
\item \emm{System Variables:}\quad $\wtV = V \cup \{t_1,\ldots,t_m,
T\}$.

Thus, $\wtV$ consists of the system variables of $\Fsysp$, to
which we add $m+1$ clocks, one clock $t_i$ for each process $P_i$,
$i=1,\ldots,m$, plus the master clock $T$.

\item \emm{Initial Condition:}\quad
$\wtTheta\colon \quad \Theta \band t_1=\cdots = t_m = T =0$.

\item \emm{Transitions:}\quad
$\wtTau\colon \bigl\{\wttau \mid \tau\in\Tau - \{\tauI\} \bigr\}$.

Let $\tau\in\Tau - \{\tauI\}$ be a transition corresponding to an
executable statement in process $P_i$. The transition relation for
transition $\wttau$ is given by:
\[\wt{\rho_{\tau}}\colon \quad \rho_\tau \band t_i\ge l_{\tau} \band
t\pri_i =0 \band \pres(t_1,\ldots, t_{i-1}, t_{i+1},\ldots, t_m, T).\]

Thus, the transition can be taken only when $t_i$, the clock
correponding to process $P_i$, is not below $l_\tau$, the lower bound
associated with $\tau$. When taken, the transition resets clock $t_i$
to 0.

\item \emm{Time-progress condition $\Pi$:}\quad
For each executable statement
\[ \ell\colon S\]
in process $P_i$, $\Pi$ includes the conjunct
\[ \ell\in\pi \quad\implies\quad t_i<\us,\]
where $\us$ is the upper bound associated with statement $S$. This
ensures that control cannot wait at location $\ell$ for more than
$\us$ without the transition associated with $S$ (or another
transition causing control to move away from $\ell$) being taken.

\end{itemize}
Note that the lower bounds of statements are added as constraints to
transitions, while the upper bounds are added as constraints to the
time-progress condition $\Pi$.

\begin{example}\quad
Figure~\ref{anyy} presents a simple program consisting of two
processes communicating by the shared variable $x$.

\begin{figure}[hbtp]
\begin{center}
\fbox{
$
\begin{array}{c}
x, y\colon\ \bold{integer\ where}\ x=y=0\\
\quad\\
\begin{array}{ccc}
%P_1::\ \ 
\left[\begin{array}{ll}
\ell_0: & \bold{while}\ x=0\ \bold{do}\\
\multicolumn{2}{l}{
\quad\ell_1:\ y:=y+1}\\
\ell_2: 
\end{array}\right]
& \quad\PLL\quad &
%P_2::\ \ 
\left[\begin{array}{ll}
m_0: & x:= 1\\
m_1: &
\end{array} \right]\\
\quad\\
-\quad P_1 \quad - & & -\quad P_2 \quad -
\end{array}
\end{array}
$
}
\caption{\label{anyy} Program {\sc any-y}.}
%
\end{center}
\end{figure}
To make it an \splt\ program, we uniformly associate each of its
executable statements with the time bounds $[3,5]$. The \ctss\
$\Phi_{\mbox{\tiny ANY-Y}_{[3,5]}}$ associated with \anyce\ is defined
as follows:
\begin{itemize} 

\item \emm{System Variables:}\quad $V = \{\pi, x, y, t_1, t_2, T\}$.
In addition to the control variable $\pi$ and data variables $x$ and
$y$, the system variables also include clock $t_1$, measuring delays
in process $P_1$, clock $t_2$, measuring delays in process $P_2$, and
the master clock $T$, measuring time from the beginning of the
computation.

\item \emm{Initial Condition:}\quad 
\[\begin{array}{lcl}
\Theta & :\quad & \pi = \{\ell_0, m_0\} \lwedge x=y=0 \lwedge t_1=t_2=T =0.
\end{array}\]

\item \emm{Transitions:}\quad $\Tau: \{\ell_0,\ell_1,m_0\}$ with
transition relations:
$$\begin{array}{ll}
\rho_{\ell_0}: & \ell_0 \in \pi \lwedge 
	\left(\begin{array}{c}
	x=0\ \wedge\ \pi'=\pi-\{\ell_0\}\cup\{\ell_1\} \\
		\vee\\
	x\neq 0\ \wedge\ \pi'=\pi-\{\ell_0\}\cup\{\ell_2\}
\end{array}\right) \lwedge t_1\ge 3 \lwedge t_1\pri = 0 \ \ \\
& \multicolumn{1}{r}{\lwedge \pres(V-\{\pi, t_1\})}\\
\quad\\[-7pt]
\rho_{\ell_1}: & \ell_1\in\pi \lwedge
	\pi'=\pi-\{\ell_1\}\cup\{\ell_0\} \lwedge y'=y+1
\lwedge t_1\ge 3 \lwedge t_1\pri = 0\\[2pt]
& \multicolumn{1}{r}{\lwedge\ \pres(V-\{\pi, y, t_1\})}\\[4pt]
%\quad \\
\rho_{m_0}: & m_0\in\pi \lwedge \pi'=\pi-\{m_0\}\cup\{m_1\} \lwedge x'=
1 \lwedge t_2\ge 3 \lwedge t_2\pri = 0\\[2pt]
& \multicolumn{1}{r}{\lwedge\ \pres(V-\{\pi, x, t_2\}).}
\end{array}$$

\item \emm{Time-progress condition:}\quad
\[\begin{array}{lcl}
\Pi & :\quad & (\atl{0,1}\ \to\ t_1< 5) \lwedge (\atm{0}\ \to\ t_2< 5)
\end{array}\]

\end{itemize}
The \tick\ transition for this system is given by
\[\begin{array}{ll}
\tick\colon\quad \exists\D>0 \St & \pres(\pi,x,y) \band
(t_1\pri,t_2\pri,T\pri) = (t_1+\D,t_2+\D,T+\D) \band\\
& (\atl{0,1}\ \to\ t_1+\D\le 5) \band (\atm{0}\ \to\
t_2+\D\le 5)\ \corn
\end{array}
\]
\end{example}

\subsection{Specification Language}

To specify properties of reactive systems, we use the language of
temporal logic, as presented in \cite{MPB}.
We use only the following:

\begin{itemize}
\item \emm{State formulas} (\emm{assertions}) - any first-order
formula. For locations $\ell_i$, $\ell_j$, and $\ell_k$, we denote:
$$\begin{array}{lcl}
\atl{i}&:& \ell_i\in\pi \\
\atl{j,k}&: & \atl{j} \vee \atl{k}
\end{array}$$

\item $\G p$\quad  ---\quad Always $p$, where $p$ is an assertion. We
refer to such a formula as an \emm{invariance formula}.

\item $p\entails (q\W r)$\quad ---\quad $p$ entails $q$ waiting
for $r$, where $p$, $q$, and $r$ are assertions. We refer to such a
formula as a \emm{waiting-for formula}. 

\item $p\entails \F r$\quad ---\quad $p$ entails eventually $r$, where
$p$ and $r$ are assertions. We refer to such a formula as a
\emm{response formula}.

\end{itemize}
For a state $s$ and assertion $p$, we write $s\vmodels p$ to indicate
that $p$ holds (is true) over $s$.  Let $\sigma:s_0, s_1 \ldots$ be an
infinite sequence of states, to which we refer as a
\emm{model}. For an assertion $p$, we say that $j\ge 0$, is a
\emm{$p$-position} if $s_j\models p$. Satisfaction of (the three
considered) temporal formulas over a model $\sig$ is defined as follows:
\begin{itemize}
\item A model $\sig$ satisfies the invariance formula $\G p$, written
$\sigma \models \G p$, if all positions within $\sig$ are
$p$-positions.

\item A model $\sig$ satisfies the waiting-for formula $p\entails (q\W
r)r$, written $\sigma \models p\entails (q\W r)$, if every $p$-position
$i$ within $\sig$ initiates an interval of positions, all of which satisfy
$q$. This continuous-$q$ interval can either extend to infinity or
terminate in an $r$-position which is not in the interval. That is,
$$\mbox{\rm\begin{tabular}{ll}
$\sig[i]\vmodels p$\hspace{.1cm} implies\hspace*{.1cm} &
$\sig[j]\vmodels q$ for all $j\ge i$, or\\
&  $\sig[k]\vmodels r$ for some $k\ge i$ and
$\sig[j]\vmodels q$ for all $j$, $i\le j<k$.
\end{tabular}}$$

\item A model $\sig$ satisfies the response formula $p\entails \F
r$, written $\sigma \models p\entails \F r$, if every $p$-position $i$
within $\sig$ is followed by an $r$-position $j\ge i$.

\end{itemize}

\nin
A temporal formula $\varphi$ is said to be \emm{valid over} \ctss\
$\Phi$ (or \emm{$\Phi$-valid}) if $\sigma \models \varphi$ for every
computation $\sigma$ of $\Phi$. We write $\Phi\models\varphi$ to indicate
this fact. An assertion $p$ is called $\Phi$-\emm{state valid} if it
holds at every $\Phi$-accessible state. We write $\Phi\vmodels p$ to
indicate that assertion $p$ is $\Phi$-state valid.

In the case that \ctss\ $\Phi$ is derived from an \splt\ program $P$,
we use the terms $P$-valid, $P$-state valid, and $P$-accessible as
synonymous to $\Phi_{_P}$-valid, $\Phi_{_P}$-state valid, and
$\Phi_{_P}$-accessible. We also write $P\models\varphi$ and $P\vmodels p$
to denote $\Phi_{_P}\models\varphi$ and $\Phi_{_P}\vmodels p$,
respectively. 
