\documentclass{article}
\usepackage{fullpage}
\usepackage{wasysym}
\usepackage{verbatim}
\usepackage[usenames,dvipsnames]{color}
\usepackage{graphicx}
\usepackage[bookmarks=false]{hyperref}
\usepackage[colour]{circus}
\usepackage{hijac}
\usepackage{accs_spec}

\hypersetup{colorlinks=true,linkcolor=black,citecolor=red,urlcolor=blue}

\title{Abstract {\Circus} Model for the Cruise Controller}

\author{Frank Zeyda}

\begin{document}

\maketitle

\tableofcontents

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                 Requirements                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\section{Requirements}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                 Preliminaries                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\section{Preliminaries}

%Definitions of auxiliary Z types, constants and functions.
%
%\input{Preliminaries.circus}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                               Global Constants                               %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Global Constants}

In this section we define a few global constants that are used later on in some of the calculations.
%
\input{GlobalConstants.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                             Channels for Sensors                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Channels for Sensors}

In this section we define channels for sensor events.
%
\input{SensorChannels.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                            Channels for Actuators                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Channels for Actuators}

In this section we define the channel for actuator event.
%
\input{ActuatorChannels.circus}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                              Channels for Times                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\input{TimerChannels.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                               Internal Channels                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Specification Events}

The channels in this section are used solely for specification purposes and are thus concealed in the top-level model of the cruise controller. This also makes the respective events urgent and therefore we do not need to impose deadlines of any sort on them. We require them for interaction of the specification components.
%
\input{InternalChannels.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                Model Analysis                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\input{ModelAnalysis.tex}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                Abstract Model                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Abstract Model}

In this section we present the abstract model of the cruise controller. It factors into four parallel components that capture the semantics of the state diagram, speed monitor, throttle controller, and timing requirements.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{State Machine}

In this section we specify the process that corresponds to the state transition diagram.
%
\input{StateMachine.circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interarrival Times}

In this section we specify inter-arrival times of events.
%
\input{InterArrivalTimes.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Speed Monitor}

In this section we specify the behaviour of the abstract component that monitors the speed.
%
\input{SpeedMonitor.circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Throttle Controller}

In this section we specify the behaviour of the abstract component that controls the throttle.
%
\input{ThrottleControl.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Timing Requirements}

In this section we specify various timing requirements of the cruise control system. They are on one hand response times when the system must acquire (or release) control of the throttle, and on another specify the maximum delay between two $set\_voltage$ events when cruising or accelerating. Informal descriptions of the requirements imposed by particular process actions are included in Table~\ref{tab:informaltimingreq}.
%
\input{ThrottleTiming.circus}

\begin{table}
\centering
\begin{tabular}{c c}
  \textbf{Process Action} & \textbf{Informal Description}\\
\hline
\hline
   $TReq1$ &
   \parbox{0.6\textwidth}{
   \smallskip
   When the user requests that cruise mode should be activated, the system should be in control of the speed within $activate\_deadline$ seconds.
   \smallskip}\\
\hline
   $TReq2$ &
   \parbox{0.6\textwidth}{
   \smallskip
   When the user requests that cruise mode should be deactivated, the system should give up control of the speed within $deactivate\_deadline$ seconds.
   \smallskip}\\
\hline
   $TReq3$ &
   \parbox{0.6\textwidth}{
   \smallskip
   When the user requests that acceleration mode should be activated, the system should be in control of the speed and accelerating within $start\_acceleration$ seconds.
   \smallskip}\\
\hline
   $TReq4$ &
   \parbox{0.6\textwidth}{
   \smallskip
   When the user requests that acceleration mode should be deactivated, the system should be in control of the speed and cruising within $stop\_acceleration$ seconds.
   \smallskip}\\
\hline
   $TReq5$ &
   \parbox{0.6\textwidth}{
   \smallskip
   When the user requests that cruise mode should be resumed, the system should be in control of the speed within $resume\_deadline$ seconds.
   \smallskip}\\
\hline
   $TReq6$ &
   \parbox{0.6\textwidth}{
   \smallskip
   Writes of the throttle voltage must occur with a certain frequency while the system is in control. We thus constrain the maximum delay between two writes to be $set\_voltage\_max\_delay$.
   \smallskip}\\
\hline
   $TReqWriteVoltage$ &
   \parbox{0.6\textwidth}{
   \smallskip
   This requirement is an artifact of the model. It states that the $set\_voltage$ event must occur immediately after $write\_voltage$. It justifies the use of $write\_voltage$ rather than $set\_voltage$ in the other timing requirements.
   \smallskip}\\
\hline
\end{tabular}
\caption{Informal description of the timing requirements for the throttle.}
\label{tab:informaltimingreq}
\end{table}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Complete System}

In this section we specify the top-level system model.
%
\input{System.circus}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                Previous Model                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\section{Previous Model}

%The previous centralised process for the abstract model of the cruise controller system is given below.
%
%\input{PreviousModel.circus}

%\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                 Bibliography                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliographystyle{plain}

\bibliography{accs_spec}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                   Appendix                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix

\section{Appendix}
\label{apx:asms}

\subsection{State Diagram 1:~Blocking Version}
\label{apx:asm1}

\begin{center}
\vspace{1ex}
\includegraphics[scale=0.77,trim=20 65 20 80,clip]{CruiseControllerAMS1.pdf}
\end{center}

\nid The blocking version of the state machine is closest to the state machine model presented in \cite{Wel04}. However, its implementation is more complex since it requires a more subtle control of interrupts.

\subsection{State Diagram 2:~Nonblocking Version}
\label{apx:asm2}

The nonblocking version of the state machine is the model that was actually implemented in \cite{Wel04}.
%
\begin{center}
\vspace{1ex}
\includegraphics[scale=0.77,trim=20 65 20 80,clip]{CruiseControllerAMS2.pdf}
\end{center}
%
\nid In \purple{purple} we highlight events that we do not expect to take place. Nonetheless we require the application to deal with them in a way that they are ignored. Important is here that even though we think of those events constraining the environment, we do not diverge if the environment does not `behave'.

\end{document}
