\chapter{System Model}

We consider two vehicles, moving along a single track. While the
behavior of the leading vehicle is arbitrary, the second vehicle's
controller must make sure that no ``bad'' collisions occur. ``Bad''
collisions are collisions at a high relative speed. This is called the
{\em Safety} requirement for the second controller. This {\em Safety}
requirement is general for all vehicle maneuvers, and is independent
of the particular algorithm used. We devise the most nondeterministic
{\em safe} controller, so that later we can use this controller as a
correctness check: a controller implementing any vehicle maneuver must
implement our {\em safe} controller in order to be correct. This should be useful in formally proving correctness of complicated algorithms.

\section{Vehicles}

\begin{figure*}[htp]
\center{\PSbox{Fig/Slide1.PS hscale=70 vscale=70}{5.8in}{1.2in}}
\caption{Vehicles}
\label{pic:vehicles}
\end{figure*}

\begin{figure}[htp]

\begin{myiotab}

{\bf Constants:} \+\\
        $l_i$, the length of the vehicle \\
        $a_{min} \in \negr$, the maximum emergency deceleration \-\\

{\bf Variables:} \+\\
        Input:\>\>
          $acc_i \in \reals$, initially arbitrary\\
        Output: \+\+ 
        $x_i \in \nnr$, initially $x_2 = 0$ and $x_1$ is arbitrary,
subject to $x_1 \geq x_2 + l_2$ \\
        $\dot{x_i} \in \nnr$, initially arbitrary \\        
        $\ddot{x}_i \in \reals$, initially arbitrary\\
        
        {\em now}, initially $0$ \\
        {\em collided}, Boolean, initially {\em false} \-\-\-\\
 
{\bf Actions:} \\

\>      Internal:\>\>\> ${collide}$\+\+\+\+\\

        Pre:\>\>        $x_1 = x_2 + l_2$ \\
        \>\>    ${collided} = {false}$ \\
        Effect:
        \>\>    $\ddot{x}_i :=$ arbitrary value, subject to
        $\ddot{x}_i \geq a_{min}$\\
        \>\>    $\dot{x}_i := $ arbitrary value\\
        \>\>    ${collided} := {true}$ \-\-\-\-\\

{\bf Trajectories:} \+\\
        an $I$-trajectory $w$ is included among the set of nontrivial trajectories exactly if \+\\
        1. ${collided}$ is unchanged in $w$ \\
        2. $\ddot{x}_i$ is integrable in $w$ \\
        3. for all $t \in I$ the following hold:\+\\
                  3.1. If ${collided} = {false}$ in $w$ then \\

                           \>$ w(t).\ddot{x}_i = max(w(t).acc_i,
                           a_{min})$\\
                           \> else, $w(t).\ddot{x}_i \geq a_{min}$ \\
                  3.2. $ w(t).\dot{x}_i = w(0).\dot{x}_i + {\int_{0}}^{t}w(u).\ddot{x}_idu$\\
                  3.3. $w(t).x_i = w(0).x_i + {\int_{0}}^{t}w(u).\dot{x_i}du$\\
                  3.4. $w(t).x_2 + l_2 \leq w(t).x_1$\\
                  3.5. $w(t).now = w(0).now + t$\\
                  3.6. If $w(t).x_1 = w(t).x_2 + l_2$ and $t$ is not the right endpoint of $I$ then \\
                \>${collided} = {true}$.\\
\end{myiotab}

\caption{The \atsAA Hybrid Automaton}

\label{fig:c-vehicles}

\end{figure}

We compose our system of a piece modeling the physical
vehicles, and two pieces modeling the controllers of each vehicle. Each piece is
modeled by a hybrid automaton. The real world piece is called \atAA. 

\begin{automaton}{\aatAA}
The automaton represents two vehicles, named $1$ and $2$, where
vehicle $1$ precedes vehicle $2$ on a single track. Positions on the
track are labeled with nonnegative reals, starting with $0$ as a
designated starting point, as shown in Figure \ref{pic:vehicles}. 
The formal HA model for this automaton is given in Figure
\ref{fig:c-vehicles}. We assume that $i \in {1, 2}$ throughout the model.

\paragraph{Constants}
\begin{itemize}
\item
$l_i$ is the length of the $i$-th vehicle.
\item
$a_{min} < 0$ is the maximum deceleration rate for the vehicles. We
assume here that all vehicles have identical breaking capabilities.
\end{itemize}

\paragraph{Variables} 
\begin{itemize}
\item $acc_i$ denotes the
acceleration commanded by the controller. Note that it can differ from
$\ddot{x}_i$, which is the actual acceleration of the vehicle, due to
delays and/or uncertainties.
\item  $x_i$, $\dot{x}_i$, and $\ddot{x}_i$ model the actual
  position of the vehicle's rear, its velocity and acceleration data. The dots
  are used as a syntactic device only, and do not impose differential
relationships.  
\item {\em now} models the current time. While it is not
necessary for modeling the system, it will be used later in stating
some of the invariant assertions. Initially, {\em now }$= 0$.
\item {\em collided} keeps track of the first occurrence of a
collision; it will be used in our statement of the correctness
property --- in this work we only want to guarantee safety for zero or
one collisions, the multiple collisions case is not handled.
\end{itemize}

\paragraph{Actions} The action {\em collide} occurs when the vehicles
touch each other for the first time. The vehicles touch when the
position of the rear of the leading vehicle, $x_1$, equals the position
of the front of the trailing vehicle, $x_2 + l_2$. The effect is that
both the vehicle's acceleration and velocity assume arbitrary values.
After the collision, the vehicle's acceleration, $\ddot{x}_i$, is decoupled from what is
commanded by the controller, while velocity and position are still
obtained by integrating the acceleration, $\ddot{x}_i$.

\paragraph{Trajectories}
The first condition (1) states that {\em collided} can only be changed
by discrete actions. Condition (2) requires the actual acceleration of the
vehicles to be integrable, so that velocity and position can be
derived from it. (3) gives conditions on all states of a trajectory.
Condition (3.1) ensures that the
vehicle implements the controller's acceleration (taking care not to
go below $a_{min}$), before the first collision occurs. Conditions
(3.2) and (3.3) give differential relationships between the actual acceleration,
velocity and position of the vehicle at all times. (3.4) does not allow
vehicles to bypass each other, which is realistic assuming that the
vehicles move only in a single lane. (3.5) assigns the variable {\em
  now}, and (3.6) makes sure that when the vehicles collide, then either
a) it is the right endpoint of the trajectory, and the {\em collide}
action will be scheduled (this happens for the first collision), or b) it is after
the first collision, and {\em collided} already is {\em true}.

\paragraph{HA}
By discussion in Section \ref{sec:model}, we only need to show that
axioms $T2$ and $T3$ are satisfied. Since the duration of trajectories
is not restricted, ``sub''-trajectories are always valid, so $T2$ is
satisfied. The only time trajectories are {\em required} to stop is
when a {\em collide} action has to occur. But by trajectory condition
(3.6), we allow these trajectories to be closed, so $T3$ is also satisfied.
Therefore, this automaton is an {\em HA}. 

\paragraph{Properties}
From this definition, several useful properties of all reachable state
of the \atsAA automaton can be deduced:
\begin{enumerate}
\item 
$\ddot{x}_i \geq a_{min}$, by trajectory condition (3);
\item
velocity and position are integrals of $\ddot{x}_i$, except at the
time of collision, by trajectory
conditions (4) and (5);
\item
$x_2 + l_2 \leq x_1$, meaning that vehicles never bypass each other, by trajectory condition (6).
\end{enumerate}

\end{automaton}

\section{Controllers}

\begin{figure}[htp]

\begin{myiotab}

{\bf Variables:} \+\\

        Input:  \>\>\>    $\ddot{x}_i \in \reals$, $i \in \{1,2\}$ \\      
                \>\>\>    $\dot{x}_i \in \nnr$, $i \in \{1,2\}$ \\
                \>\>\>    $x_i \in \nnr$, $i \in \{1,2\}$\\
        Output: \>\>\>    $acc_j$, initially arbitrary, where $acc_j \geq a_{min}$\\
        Internal: \>\>\>  $\dot{x}_{intj} \in \nnr$, 
                                initially $\dot{x}_{intj} = \dot{x}_j$ \\
                \>\>\>    $x_{intj} \in \nnr$,
                                initially $x_{intj} = x_j$ \-\\

{\bf Trajectories:} \+\\

        an $I$-trajectory $w$ is included among the set of nontrivial
        trajectories exactly if \+\\
        1. $\mathit{acc}_j$ is an integrable function \\
        2. for all $t \in I$, in state $w(t)$ \+\\
                  2.1. $\dot{x}_{intj} = w(0).\dot{x}_{intj} + {\int_{0}}^{t}w(u).acc_{j}du$\\
                  2.2. $x_{intj} = w(0).x_{intj} + {\int_{0}}^{t}w(u).\dot{x}_{intj}du$\\
                  2.3. If $\dot{x}_j \leq 0$ then $acc_j \geq 0$\-\-\\
\end{myiotab}

\caption{${Controller}_j$ Hybrid Automaton, $j \in \{1,2\}$}

\label{fig:controller1}

\end{figure}

We now define the controller automaton.

\begin{automaton}{\aatB, $j \in \{1, 2\}$}
This automaton inputs the current position, velocity and acceleration
data of the vehicle (from the \atsAA automaton) and outputs
new acceleration settings.
It is an arbitrary hybrid automaton with the
given interface, and it is restricted only by the physical limitations of
the vehicles. It does not have any discrete actions.
The formal model for this automaton, where $j$ is either 1 or 2, is
given in Figure \ref{fig:controller1}. 

\paragraph{Variables} \atsB receives the
real position and velocity data of both vehicles via sensors, which we
model by inputing the data from the \atsAA automaton. Based
on these inputs, the \atsB decides on a safe acceleration setting
and outputs it to \atAA.
The internal velocity and position variables ($\dot{x}_{intj}$ and
$x_{intj}$) are approximations to the real data of \atAA,
calculated based on the acceleration the \atsB has commanded. This data
is obtained by integrating the acceleration requests of the
controller. Since we have not included any delays or uncertainties
yet, these variables should correspond exactly to the actual position
and velocity of the vehicle, so that $x_{intj} = x_j$ and
$\dot{x}_{intj} = \dot{x}_j$. However, when we add uncertainty
and delay into our model, the internal variables will be different
from the input variables (which are received from sensors); the
internal variables will use input variables and account for delays and
uncertainties to get better estimates of the actual data.

\paragraph{Trajectories}
Condition (1) requires that the commanded acceleration be integrable
twice, so that the integrals for velocity and position are well
defined. Conditions (2.1)
and (2.2) define internal velocity and position data to be integrals of
commanded acceleration. Finally, condition (2.3) guarantees that once the vehicle
has non-positive velocity, the acceleration must be non-negative, keeping the vehicles from going backwards.

\paragraph{HA}
No restrictions on either the duration of a trajectory, or stopping
trajectories are places, so axioms $T2$ and $T3$ are satisfied. Thus,
by discussion in Section \ref{sec:model}, \atsB is an {\em HA}.

\end{automaton}

\begin{figure*}

\center{\PSbox{Fig/Slide2.PS hscale=75 vscale=75}{3.6in}{2.0in}}

\caption{\atsE Model}

\label{fig:contr}

\end{figure*}

We model the whole system by composing the \atsAA automaton
with 2 controllers. These controllers must be implementations of \atB. Thus, the composed
system is a ``function'' of the given controllers and the given
implementation of the \atsAA automaton.

\begin{automaton}{\aatE}
\atE($V$, $A_1$, $A_2$) = \atsAA $\parallel A_1 \parallel A_2$, where $V$ is an
implementation of the \atsAA automaton, $A_1$ is an
implementation of \atC, and $A_2$ is an implementation of \atD. The
automata are composed using hybrid automata composition rules,
resulting in another {\em HA} automaton. The
system models our vehicle system with each vehicle
having its own controller. Figure \ref{fig:contr} shows \atE(\atAA,
\atC, \atD), by showing the pieces it
consists of and the interfaces between them.
\end{automaton}

\section{Safety Condition}

We define a safety condition for the states of \atE. The safety condition guarantees that if the
vehicles ever collide, then the first time they do so, their relative
velocity is no more than $v_{allow}$. We formulate this condition
formally as an invariant assertion:

\begin{definition}{Safety}
If $x_1 = x_2 + l_2$ and {\em collided} = {\em false}, then
$\dot{x}_2  \leq \dot{x_1} + v_{allow}$.
\end{definition}

We define a new automaton, \atF, to serve as a
correctness specification. 

\begin{automaton}{\aatF} 
This automaton is exactly the same as
\atsAA with an added restriction on trajectories:
all states are required to satisfy the {\em Safety} condition. Since
this restriction does not violate axioms $T2$ and $T3$, the \atsF
automaton is still a valid {\em HA}.
\end{automaton}

Given an implementation $V$ of \atAA, we want to design an implementation
$A_2$ of \atsD such that for any implementation $A_1$ of \atC, the
system \atE($V$, $A_1$, $A_2$) implements the \atsF automaton. Then we
can say that it satisfies the {\em Safety} condition. 
That is enough to ensure that the {\em
  Safety} condition of the specification carries over to the
implementation. Note that although the \atsE automaton includes
controllers, it can still implement the \atsF automaton, since they
will have the same external interface (position, velocity,
acceleration data, the $now$ variable, and the {\em collided} flag) and the controllers only affect
the acceleration settings.

\begin{definition}{Correctness}
\label{def:correctness}
Given an implementation $V$ of \atAA, an implementation $A_2$ of \atsD
is {\bf correct} for $V$ if and only if for every implementation $A_1$ of
\atC, \atE($V$, $A_1$,$A_2$) system implements \atF. 
\end{definition}










%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
