Project_1.tex

\documentclass{article}
\usepackage{times}
\usepackage{fullpage}

\newcommand{\head}{\subsection*}
\setlength{\parindent}{0pt}

\begin{document}

%_______________________________________________________________________________
% Heading section
%_______________________________________________________________________________
\begin{center}
\rule{\textwidth}{1.5pt} \\ \rule[10pt]{\textwidth}{1pt}\\
Innopolis Univerrsity \hfill Models of Software Systems\\[3ex]
{\Large\bf Project 1: State Machine Modeling}\\[3ex]
Group 2 \hfill {\bf Due: October 02, 2017} \rule{\textwidth}{1pt}
\\\rule[9.5pt]{\textwidth}{1.5pt}
\end{center}

The purpose of this first project is to give you experience in
modeling a realistic system as a state machine. The example that we
will use is the Infusion Pump. A general description of an Infusion
Pump can be found in \textit{Project} folder on Moodle. 

\bigskip You should carry out this project in your assigned team. Make sure that
everyone in the group contributes to the overall effort. Each team should submit a
single write-up of the project, due at the beginning of class on the project due
date. We have posted a template for a group project write-up under the
\textit{Resources} section on Moodle.

%___________________________________________________________________________________________________
\head{Task 1 (20 points):}
%___________________________________________________________________________________________________

A sample description of a \emph{simplified version} of an infusion
pump, written in FSP, is provided with this project document. This
model describes a pump with only one infusion channel, and leaves
out many of the features that a real infusion pump would have, as
outlined in the general infusion pump description.

\bigskip Your first task is to understand this specification. Read
through the specification to make sure you understand what it is
specifying. Then read it into LTSA and check its behavior using the
LTSA simulation capabilities. Once you are familiar with it, answer
the following questions in your project write-up:

\begin{enumerate}
    \item What is the alphabet of the state machine?
    
    \textbf{Answer:}\\
    $\{plug\_in, turn\_on, unplug, turn\_off, set\_rate, enter\_value, press\_set, press\_cancel, clear\_rate,\\ connect\_set, purge\_air, lock\_line, confirm\_settings, erase\_and\_unlock\_line, change\_settings\\
    lock\_unit, unlock\_unit, dispense\_main\_med\_flow, flow\_blocked, sound\_alarm, silence\_alarm\\
    flow\_unblocked\}$

    \item List two traces of the pump, each at least 4 actions in length.
    
    \textbf{Answer:}\\
    $\langle plug\_in, turn\_on, set\_rate, enter\_value, press\_set, connect\_set, purge\_air, lock\_line, confirm\_settings\rangle$
    $\langle plug\_in, turn\_on, set\_rate, enter\_value, press\_cancel\rangle$
    
    \item In contrast to the specification of an infusion pump in homework 6, how does this specification model the fact that     the pump might run out of liquid?
    
    \textbf{Answer:} In provided specification amount of liquid is considered to be infinite.
    
    \item Is it possible to ever dispense medication without setting the rate?  Why or why not? If your answer is yes, provide a trace that justifies your answer.
    
    \textbf{Answer:} No, it is impossible, because without setting up parameters $params == ParamsSet$ and without locking line $lineLock == LineLocked$ we can't proceed to infusion mode.
    
    \item Is it ever possible for the flow to become blocked and have the alarm not sound at all?  Why or why not? If your answer is yes, provide a trace that justifies your answer.
    
    \textbf{Answer:} No, it is impossible, because after $flow\_blocked$ the only possible action is $sound\_alarm$.
    
    \item If the pump is locked and dispensing, without unlocking or becoming blocked, will the pump ever stop dispensing? If your answer is yes, provide a trace that justifies your answer.
    
    \textbf{Answer:} Yes if the pump will become unplugged or turned off. Example with unplug case:\\
    $\langle plug\_in, turn\_on, set\_rate, enter\_value, press\_set, connect\_set, purge\_air, lock\_line, confirm\_settings,\\lock\_unit, dispense\_main\_med\_flow, unplug\rangle$
    
    \item If the pump is locked and dispensing, is it possible for the \emph{patient} to alter the medicine he is receiving? If your answer is yes, provide a trace that justifies your answer.
    
    \textbf{Answer:} No. Changing of settings is possible only when the pump is in unlocked state.
    
    \item Does this version have any behavior that you feel is inconsistent with the pump specification? Could it be fixed?
    
    \textbf{Answer:} Yes, it has inconsistencies and we will show our fixes in Task 2.
    
\end{enumerate}

%___________________________________________________________________________________________________
\head{Task 2 (75 Points):}
%___________________________________________________________________________________________________

For the second part of your project you should develop a
more-complete FSP specification of the infusion pump (40 points). To
do this you can use the sample of Task 1 as a starting point, or you
can start with your own model. Here are some guidelines to keep in
mind as you develop your FSP specification:

\begin{itemize}
\item You do not need to model the human user of the pump.

\item Restrict your specification to a single-line infusion pump.

\item You are free to pick the level of abstraction for this specification. Your specification
should be detailed enough, however, to answer the questions posed below.

\item Be sure to document your specification adequately, and choose meaningful action and process names for readability.

\item Your specification should not use parallel composition.

\end{itemize}

\noindent The full specification should be attached to your project
write-up. Answer the following questions (25 points); for each,
briefly explain why you answered it in the way you did, based on
\emph{your} model. If your model does not address this issue,
explain why. (Note: Reference certain parts of your specification that address features, ambiguities, or errors in each question.)

\begin{enumerate}
    \item Which aspects of the pump did you choose to model, and which did you choose to leave out? \\
    \textbf{Answer:} The following is modelled in our specifications:
    \begin{enumerate}
        \item power outage when the pump is administering medications
        \item alarm when pump is operating using the battery and battery is depleting
        \item sleep mode when no user interaction is happening during long periods of time when it's needed (some parameters have not been set yet, for example)
        \item drug library
    \end{enumerate}
    The rest of specifications is not modeled, including
    \begin{enumerate}
        \item overheating
        \item battery charge error
        \item etc.
    \end{enumerate}
    \item Were there ambiguities in the English description of the infusion pump that your specification resolves?\\
    \textbf{Answer:} There are some. For example it does not state what happens when electrical failure occurs and battery is uncharged. It says only that transition does not happen. In the proposed model we suppose that battery is properly charged, so that it's never the case that battery is uncharged immediately when power goes off (assuming battery has been charging).
    
    \item State four general properties that your pump guarantees (for example, the alarm will always sound if a line becomes clogged), and say briefly why it is guaranteed. \\
    \textbf{Answer:} The following is guaranteed by our specifications:
    \begin{enumerate}
        \item whenever battery power goes too low either the alarm sounds or pump get connected to grid immediately, because only these transitions are possible at that moment
        \item user can reset the device settings only when it is operating using external power supply (for safety reasons), because transition to settings of pump is not specified when pump is using battery
        \item whenever power outage happens the pump notifies the personnel by the visual signal and switches to battery, cause that's the only option at that moment
        \item hard and soft limits get checked every time the pump is started up using some drug values, because only through that check it's possible for the pump to reach delivering medication mode 
    \end{enumerate}
    
    \item Does your model say what happens if the power goes out in the middle of operation? 
    \\
    \textbf{Answer:} Yes. The proposed model describes how the pump must behave when power goes off when pump is delivering the medications. 
    \\However, it does not consider the case when the power goes off when medical stuff sets the parameters. Because it's much more important to change power source when a pump is working and there's no medical personnel nearby. If not all of the parameters are set, then personnel shall handle the error before starting a pump up. 
    \item Referring to the additional documentation about the infusion pump on the general project description section of the web site, consider the errors noted about realistic pumps. Which of these types of errors can be illustrated with your pump? Does your pump exclude some of them from happening?

\end{enumerate}


%___________________________________________________________________________________________________
\head{Task 3 (5 points):}
%___________________________________________________________________________________________________


How difficult would it be using the current subset of FSP to create
a 4-line pump? What would have to change in your specification?\\

Suppose that different lines should work independently. It means that different works should be run at the same time. Because of that, we have to use a parallel state machine. This is not allowed in our task.\\
Assume that it is allowed. We think that the main trouble with a parallel 4-line pump would be input/output operations. What should happen if we switch line during input? Should input save state? Also, there would be some troubles with alarm speaker: How it should work if some problems happen on 2 lines in same time? How to manage situation when we solve problem on one line but in another line problem still be?\\
In conclusion, we think that most of the problems with parallel work caused by shared resources and synchronization points.


\end{document}