\chapter{Conclusion and Future Work}

The system consisting of two vehicles moving on a single track has
been modeled using hybrid automata, including all the components
(physical vehicles, controllers, delay and uncertainty buffers), and
the interactions among them. Safety conditions were formulated using
invariant assertions. Correctness and optimality of controllers were
proved using composition, simulation mappings and invariants, and the
methods of mathematical analysis. Complexity (delays and uncertainty)
was introduced gradually, using levels of abstraction, significantly simplifying the proofs.

The case study formally describes a general controller that is
necessary and sufficient to guarantee the safety requirement regardless of
the behavior of the leading vehicle. Such a controller can be later
reused to prove correctness of complicated maneuvers, such as merging
and splitting, where the setup is similar.

There are two important results of this research. Generally, it
demonstrates the power of the hybrid automata model, the associated proof
methods in reasoning about interesting hybrid systems, and the use of
abstraction levels as a way of handling complexity. More
specifically, we give a reusable model of the automated vehicles, including
their controllers and sensors, which incorporates delays and uncertainties
directly, and we derive and prove necessary and sufficient conditions
for satisfying the safety requirement of the vehicles.

Future work will address the following problems:
\begin{enumerate}
\item
In reality, the controllers can only control
the jerk, and not the acceleration of the vehicles. Without further
complicating the models, we can still model the controllers as
controlling the acceleration, but the outbound delay (and, possibly,
uncertainty) have to be increased to account for the fact that it
takes some time for the controller to reach desired acceleration.
Using this approach, the outbound delay and/or uncertainty might
become functions of current acceleration, and not constants.
\item
We have developed necessary and sufficient conditions for a controller
to guarantee safety in the presence of delays and uncertainties. This
controller can now serve as a correctness specification.
We could prove correctness of ``real'' algorithms, for merging or
splitting, by testing them with our controller.
\item
In this thesis we only handled the first collision, when in fact, even
in the case of two vehicles, multiple collisions can occur. Although
all of the models do not have to be changed, most of the proofs would have to
be reworked to handle this case. This would be similar to Lygeros and
Lynch's work in \cite{Lygeros-strings}, but would have more
detailed vehicle models, including delays and uncertainties.
\item
Finally, it would be interesting to extend the models and the proofs
to the multiple vehicle case. If we limit the analysis to only
pairwise collisions (excluding simultaneous collisions of three or more
vehicles), then the models and some of the analysis from this thesis can
be reused, but many new problems would arise. In order to remove the
pairwise-only collisions restriction, some of the models would
have to be reworked to model these collisions. The results would be
more general than in \cite{Lygeros-strings}, since delays and uncertainties
would be included in the model.
\end{enumerate}
