text:
\section{Background and Related Work}
\label{sec:background}

\paragraph{LTL syntax and semantics.} Linear temporal logic
(LTL)~\cite{pnueli1977} formulae
are built on a finite set $Prop$ of atomic propositions
as follows:
\begin{center}
  $\phi =$ $\bot$ $\mid$ $\top$ $\mid$ $p$ $\mid$ $\neg \phi_1$
  $\mid$ $\phi_1\vee\phi_2$ $\mid$ $\mathcal{X}
  \phi_1$ $\mid$ $\phi_1 \mathcal{U} \phi_2$
\end{center}
where $p \in Prop$, $\phi, \phi_1, \phi_2$ are LTL
formulae,  $\mathcal{X}$ is the ``next'' operator and $\mathcal{U}$ is
the ``until'' operator. An LTL formula is interpreted over
a \emph{computation}, i.e., a function $\pi: \mathbb{N} \rightarrow
2^{Prop}$ which assigns truth values to the elements of $Prop$ at
each time instant (natural number). For a
computation $\pi$ and a point $i \in \mathbb{N}$:
\begin{itemize}
\item $\pi, i \not\models \bot$ and $\pi, i \models \top$
\item $\pi, i \models p$ for $p \in Prop$ iff $p \in \pi(i)$
\item $\pi, i \models \neg \alpha$ iff $\pi, i \not\models \alpha$
\item $\pi, i \models (\alpha \vee \beta)$ iff
    $\pi, i \models \alpha$ or $\pi, i \models \beta$
\item $\pi, i \models \mathcal{X} \alpha$ iff $\pi, i+1 \models \alpha$
\item $\pi, i \models \alpha \mathcal{U} \beta$ iff for some $j\geq i$, we have
  $\pi, j \models \beta$ and for all $k$, $i \leq k < j$ we have
  $\pi, k \models \alpha$
\end{itemize}
We say that $\pi$ \emph{satisfies} a formula $\phi$, denoted $\pi \models
\phi$, iff $\pi, 0 \models \phi$.
If $\pi \models \phi$ for every
$\pi$, then $\phi$ is \emph{true} and we write $\models \phi$.
We abbreviate as $\Diamond \phi$ (``eventually'') the formula $\top$
$\mathcal{U} \phi$ and $\Box \phi$ (``always'') the formula $\neg
\Diamond \neg \phi$. We also consider other Boolean connectives
like ``$\wedge$'' and ``$\rightarrow$'' with the usual meaning.
Finally, some of the PSPs use the ``weak until'' operator
defined as $p \mathcal{W} q = \Box p \vee (p \mathcal{U} q)$.

\paragraph{LTL satisfiability.} Among various approaches to decide LTL
satisfiability,
reduction to model checking was proposed in~\cite{rozier2007}
to check the consistency of requirements expressed as LTL formulae.
Given a formula $\phi$ over a set $Prop$ of atomic
propositions, a \emph{universal} model $M$ can
be constructed. Intuitively, a  universal model encodes all the
possible computations over $Prop$ as (infinite) traces, and therefore
$\phi$ is satisfiable precisely when $M$ does not satisfy $\neg \phi$.
In~\cite{rozier2011} a first improvement over this basic strategy is presented
together with the tool PANDA~\cite{panda},
whereas in~\cite{li2013} an algorithm based on automata construction
is proposed to enhance performances even further --- the approach is
implemented in a tool called \textsc{aalta}. Further studies along this
direction include~\cite{li2014} and~\cite{li2013b}. In the latter,
a portfolio LTL satisfiability solver called \textsc{polsat}\ is proposed to
run different techniques in parallel and return the result of the first
one to terminate successfully.

\begin{figure}\fbox{%
    \begin{minipage}[t]{0.9\textwidth}

      \begin{center}
        \textbf{Response}
        \end{center}
      Describe cause-effect relationships between a pair of
      events/states. An occurrence of the first, the cause, must be
      followed by an occurrence of the second, the effect. Also known
      as Follows and Leads-to.

      \par\noindent\rule{\textwidth}{0.4pt}

      \textbf{Structured English Grammar}

      \textsl{It is always the case that if P holds, then S eventually holds.}

      \par\noindent\rule{\textwidth}{0.4pt}

      \textbf{LTL Mappings}

      {
        \renewcommand{\arraystretch}{1.5}
         \begin{tabular}{l@{\hskip 1cm}l
         Globally & $\Box (P \rightarrow \Diamond S)$\\%\hline
         Before R & $\Diamond R \rightarrow (P \rightarrow
         (\overline{R}\
         \mathcal{U}\ (S \wedge \overline{R})))
         \ \mathcal{U}\ R$\\%\hline
         After Q  & $\Box(Q \rightarrow \Box (P \rightarrow \Diamond S))$\\%\hline
         Between Q and R & $\Box((Q \wedge \overline{R} \wedge \Diamond R)\rightarrow  (P \rightarrow (\overline{R}\ \mathcal{U}\ (S \wedge \overline{R})))\ \mathcal{U}\ R)$ \\%\hline
         After Q until R & $\Box(Q\wedge \overline{R} \rightarrow ((P\rightarrow(\overline{R}\ \mathcal{U}\ (S \wedge\overline{R})))\ \mathcal{W}\ R)$\\%\hline
        \end{tabular}
      }
      \par\noindent\rule{\textwidth}{0.4pt}
      \textbf{Example}

      \textsl{If the train is approaching, then the gate shall be closed}.

  \end{minipage}
  }%
  \caption{Response Pattern}
  \label{fig:response}

\end{figure}

\paragraph{Property Specification Patterns (PSPs).} The original
proposal of PSPs is to be found in~\cite{dwyer1999}.
They are meant to describe the essential structure of
system's behaviours and provide expressions of such behaviors in a
range of common formalism.
An example of a PSP from~\cite{specpatt} is given in
Figure~\ref{fig:response} --- with some part omitted for sake of readability.
A pattern is comprised of a \emph{Name} (Response in
Figure~\ref{fig:response}), an (informal) statement describing the behaviour
captured by the pattern, and a (structured English)
statement~\cite{konrad2005} that should be used to express requirements.
The LTL mappings corresponding to different declinations of the pattern
are also given, where capital letters (P,S,T,R,Q) stands for
Boolean states/events.\footnote{We omitted some aspects which are
  not relevant for our work, e.g., translations to other logics like
  CTL~\cite{dwyer1999}.}
In more detail, a PSP is composed of two parts: ($i$) the
\emph{scope}, and ($ii$) the \emph{body}.
The \textsl{scope} is the extent of the program execution over which
the pattern must hold, and there are five scopes allowed:
\emph{Globally}, to span the entire scope execution;
\emph{Before}, to span execution up to a state/event;
\emph{After}, to span execution after a state/event;
\emph{Between}, to cover the part of execution from one state/event to
another one;
\emph{After-until}, where the first part of the pattern continues
even if the second state/event never happens.
For state-delimited scopes, the interval in which the property is
evaluated is closed at the left and open at the right end.
The \textsl{body} of a pattern, describes the behavior that we want to
specify. In~\cite{dwyer1999} the bodies are categorized in
\emph{occurrence} and \emph{order} patterns.
Occurrence patterns require states/events to occur or
not to occur. Examples of such bodies are \emph{Absence}, where a
given state/event must not occur within a scope, and its opposite
\emph{Existence}.
Order patterns constrain the order of the
  states/events. Examples of such patterns are \emph{Precedence}, where a
  state/event must always precede another state/event, and
  \emph{Response}, where a state/event must always be followed by
  another state/event within the scope.
Moreover, we included the \emph{Invariant} pattern introduced in~\cite{post2012formalization}, and dictating that
a state/event must occur whenever another state/event occurs.
Combining scopes and bodies we can construct 55 different types of
patterns. For more details, please visit~\cite{specpatt}.

\paragraph{Related Work.}
In~\cite{lumpe2011} the framework, \textsl{Property
  Specification Pattern Wizard (PSP-Wizard)} is presented, for
machine-assisted definition of temporal formulae capturing
pattern-based system properties.
PSP-Wizard offers a translation into LTL of the patterns encoded in
the tool, but
it is meant to aid specification, rather than support consistency
checking, and it cannot deal with numerical signals.
In~\cite{konrad2005}, an extension is presented
to deal with real-time specifications, together with
mappings to Metric temporal logic (MTL), Timed computational tree
logic (TCTL) and Real-time graphical interval logic (RTGIL).
Even if this work is not directly connected with ours, it is worth
mentioning it since their structured English grammar for patterns is
at the basis of our formalism.
The work in~\cite{konrad2005} also provided inspiration to
a recent set of works~\cite{dokhanchi2016,dokhanchi2015} about
a tool, called VI-Spec, to assist the analyst in the elicitation and
debugging of formal specifications.
VI-Spec lets the user specify requirements
through a graphical user interface, translates them to MITL formulae
and then supports debugging of the specification using run-time
verification techniques.
VI-Spec embodies an approach similar to ours to deal with numerical
signals by translating inequalities to sets of Boolean variables.
However, VI-Spec differs from our work in several aspects, most
notably the fact that it performs debugging rather than consistency,
so the behavior of each signal over time must be known. Also, VI-Spec
handles only inequalities and does not deal with sets of requirements
written using PSPs.

\section{Analysis with Probabilistic Requirement Generation}
\label{sec:random}

The main goal of this Section is to investigate the scalability of our
encoding from LTL($\mathcal{D}$) to LTL.  To this end, we evaluate the
performances\footnote{All the experiments reported in this Section ran
  on a server equipped with 2 Intel Xeon E5-2640 v4 CPUs and 256GB RAM
  running Debian with kernel 3.16.0-4.} of some
state-of-the-art tools for LTL satisfiability, and then we consider
the best among such tools to assess whether our approach can scale to
sets of requirements of realistic size. Since we want to have
control over the kind of requirements, as well as the number of
constraints and the size of the corresponding domains, we generate
artificial specifications using a probabilistic model that we devised
and implemented specifically to carry out the experiments herein
presented.
In particular, the following parameters can be tuned in our
generator of specifications:
\begin{itemize}
\item The number of requirements generated ($\#req$).
\item The probability of each different body to occur in a
  pattern.
\item The probability of each different scope to occur in a
  pattern.
\item The size ($\#vars$) of the set from which variables
  are picked uniformly at random to build patterns.
\item The size ($dom$) of the domain from which the thresholds of the
  atomic constraints are chosen uniformly at random.
\end{itemize}

\paragraph{Evaluation of LTL satisfiability solvers.}
The solvers considered in our analysis are the ones included in
the portfolio solver \textsc{polsat}~\cite{li2013b}, namely
\textsc{aalta}~\cite{li2013}, \textsc{NuSMV}~\cite{cimatti2002},
\textsc{pltl}~\cite{schwendimann1998}, and \textsc{trp++}~\cite{hustadt2003}.  In order
to have a better understanding about the behavior of such solvers,
we ran them separately instead of running \textsc{polsat}. Furthermore,
in the case of \textsc{NuSMV},
we considered two different encodings. With reference to
Property~\ref{prop:key}, the first encoding defines $\phi_M$
as an invariant --- denoted as \textsc{NuSMV-invar}{} --- and $\phi'$ is the property
to check; the second encoding considers $\phi_M \rightarrow \phi$ as
the property to check --- denoted as \textsc{NuSMV-noinvar}{}.
In our experimental analysis we set the range of the parameters
as follows: $\#vars$ $\in \{16,32\}$, $dom \in \{2,4,8,16\}$, and
$\#req$ $\in\{8, 16, 32,64\}$.  For each combination of the
parameters with $v\in \#vars$, $r\in \#req$ and $d\in dom$, we generate
10 different benchmarks. Each benchmark is a specification
containing $r$ requirements where each scope has
(uniform) probability 0.2 and each body has (uniform)
probability 0.1. Then, for each atomic constraint in
the benchmark, we choose a variable out of $v$ possible ones, and a
threshold value out of $d$ possible ones.
In Table~\ref{tab:preliminary} we show the results of the
analysis.  Notice that we do not show the results of \textsc{trp++}\ because of
the high number of failures obtained. Looking at the table, we can see
that \textsc{aalta}\ is the tool with the best performances, as it is capable
of solving two times the problems solved by other solvers in most
cases. Moreover, \textsc{aalta}\ is up to 3 orders of magnitude faster than
its competitors. Considering unsolved instances, it is worth noticing
that in our experiments \textsc{aalta}\ never reaches the granted time limit (10
CPU minutes), but it always fails beforehand. This is probably due to
the fact that \textsc{aalta}\ is still in a relatively early stage of
development and it is not as mature as \textsc{NuSMV}\ and \textsc{pltl}. Most
importantly, we did not found any discrepancies in the satisfiability
results of the evaluated tools.
\begin{table}[t!]
\setlength{\tabcolsep}{2pt}
\caption{Evaluation of LTL satisfiability solvers on
  randomly generated requirements. The first line reports the size of
  the domain ($dom$), while the second line reports the total amount
  of variables ($vars$) for each domain size. Then, for each tool (on
  the first column), the table shows the total amount of solved
  problems and the CPU time (in seconds) spent to solve them (columns
  ``S'' and ``T'', respectively).}
\label{tab:preliminary}
{\scriptsize
\begin{tabular}{|l|r|r|r|r|r|r|r|r|r|r|r|r|r|r|r|r|}\hline
\multicolumn{1}{|c|}{$dom$} & \multicolumn{4}{|c|}{2} & \multicolumn{4}{|c|}{4} & \multicolumn{4}{|c|}{8} & \multicolumn{4}{|c|}{16} \\\hlin
  \multicolumn{1}{|c|}{$\#vars$} & \multicolumn{2}{|c|}{16} & \multicolumn{2}{|c|}{32} & \multicolumn{2}{|c|}{16} & \multicolumn{2}{|c|}{32} & \multicolumn{2}{|c|}{16} & \multicolumn{2}{|c|}{32} & \multicolumn{2}{|c|}{16} & \multicolumn{2}{|c|}{32} \\\hline

\multicolumn{1}{|c|}{\bf Tool} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} & \multicolumn{1}{|c|}{\bf S} & \multicolumn{1}{|c|}{\bf T} \\ \hline \hline
  \textsc{aalta} & \textbf{16} & 0.0 & \textbf{27} & 0.1 & \textbf{22} & 0.1 & \textbf{29} & 0.4 & \textbf{26} & 0.6 & \textbf{29} & 1.4 & \textbf{25} & 2.8 & \textbf{31} & 4.9 \\ \hline
  \textsc{NuSMV-invar}   & 11 & 30.4 & 10 & 185.1 & 10 & 804.2 & 9 & 881.3 & 11 & 68.1 & 8 & 402.9 & 10 & 1172.6 & 8 & 1001.9\\ \hline
  \textsc{NuSMV-noinvar} & 11 & 65.0 & 10 & 489.7 & 7 & 303.6 & 7 & 505.5 & 11 & 92.4 & 10 & 1277.6 & 8 & 660.0 & 9 & 1394.5 \\ \hline
  \textsc{pltl}        & 8 & 25.0 & 11 & 108.1 & 9 & 1.2 & 10 & 0.6 & 10 & 19.6 & 11 & 0.1 & 11 & 14.5 & 14 & 3.5 \\ \hline
\end{tabular}
}
\end{table}
\begin{figure}[p]
\begin{center}
\begin{tabular}{|l|l|}\hline
  \pgfuseimage{i1} & \pgfuseimage{i2} \\\hline
  \pgfuseimage{i3} & \pgfuseimage{i4} \\\hline
  \pgfuseimage{i5} & \pgfuseimage{i6} \\\hline
  \pgfuseimage{i7} & \pgfuseimage{i8} \\\hline
\end{tabular}
\end{center}
\caption{\label{fig:random} Scalability Analysis. On the $x$-axes
  ($y$-axes resp.) we report $\#req$ (CPU time in seconds resp.). Axis
  are both in logarithmic scale. In each plot we consider different
  values of $\#dom$. In particular, the diamond green line is for
  $\#dom$ = 4, the light blue line with stars is for $\#dom$ = 8, the
  blue crossed lines and red circled ones denote $\#dom = 16$ and
  $\#dom = 32$, respectively.}
\end{figure}
\paragraph{Evaluation of scalability.}
The analysis involves 2560 different benchmarks generated as
in the previous experiment.  The initial
value of $\#req$ has been set to 15, and it has been doubled until
1920, thus obtaining benchmarks with a total amount of requirements
equals to 15, 30, 60, 120, 240, 480, 960, and 1920. Similarly has been
done for $\#vars$ and $\#dom$; the former ranges from 5 to 640, while
the latter ranges from 4 to 32.  At the end of the generation, we
obtained 10 different sets composed of 256 benchmarks.
In Figure~\ref{fig:random} we present the results,
obtained running \textsc{aalta}. The Figure is composed by 8
plots, one for each value of $\#vars$.
Looking at the plots in Figure~\ref{fig:random}, we can see that
the difficulty of the problem increases when all the values
of the considered parameters increase, and this is particularly true
considering the total amount of requirements. The parameter
$\#dom$ has a higher impact of difficulty when the number of
variables is small. Indeed, when the number of variables is less then 40
there is a clear difference between solving time with $\#dom = 4$
and $\#dom = 32$.  On the other hand when the number of variables
increases, all the plots for various values of $\#dom$ are very close
to each other. As a final remark, we can see that even considering the
largest problem ($\#vars$ = 640, $\#dom$ = 32), more than the 60\% of
the problems are solved by \textsc{aalta}\ within the time limit of 10 minutes.

\section{Analysis with a Controller for a Robotic Manipulator}
\label{sec:robot}

In this Section, as a basis for our experimental analysis, we
consider a set of requirements from the design of an embedded
controller for a robotic manipulator. The controller should direct a
properly initialized robotic arm --- and related vision system --- to
look for an object placed in a given position and move to such
position in order to grab the object; once grabbed, the object is to
be moved into a bucket placed in a given position and released without
touching the bucket. The robot must stop even in the case of an
unintended collision with other objects or with the robot itself ---
collisions can be detected using torque estimation from current
sensors placed in the joints. Finally, if a general alarm
is detected, e.g., by the interaction with a human supervisor, the
robot must stop as soon as possible.
The manipulator is a 4 degrees-of-freedom Trossen Robotics WidowX
arm\footnote{Technical specifications are available at
  \url{http://www.trossenrobotics.com/widowxrobotarm}.} equipped
with a gripper: Figure~\ref{fig:robot} shows a snapshot of the robot
in the intended usage scenario taken from
V-REP\footnote{\url{http://www.coppeliarobotics.com/}} simulator.
The design of the embedded controller is currently
part of the activities related to the ``Self-Healing System for
Planetary Exploration'' use case~\cite{masin2017cross} in the context
of the EU project CERBERO.

\begin{table}[t!]
  \begin{tabular}{|l|r|r|r|r|r|r|} \hline
    \multicolumn{1}{|c|}{\textbf{Pattern}} &
    \multicolumn{3}{|c|}{Specification} & \multicolumn{3}{|c|}{Fault
      injections} \\ \cline{2-7}
    \multicolumn{1}{|c|}{\ } & \multicolumn{1}{|c|}{\textsc{after}} &
    \multicolumn{1}{|c|}{\textsc{after\_until}} &
    \multicolumn{1}{|c|}{\textsc{globally}} &
     \multicolumn{1}{|c|}{\textsc{after}} &
     \multicolumn{1}{|c|}{\textsc{after\_until}} &
     \multicolumn{1}{|c|}{\textsc{globally}} \\ \hline\hline
    Absence  & -- & 12 & 14 & [F4] & -- & [F3] \\ \hline
    Existence & 9 & -- & -- & -- & [F5] & [F4, F6] \\ \hline
    Invariant & -- & -- & 29 & -- & -- & [F2, F6]\\ \hline
    Precedence  & -- & -- & 1 & -- & -- & -- \\ \hline
    ResponseChain & -- & -- & 2 & -- & -- & -- \\ \hline
    Response & 1 & -- & 4 & -- & -- & [F1] \\ \hline
    Universality & 2 & -- & 1 & -- & -- & -- \\ \hline

  \end{tabular}
  \caption{  \label{tab:robot-req}%
    Robotic use case requirements synopsis. The table is
    organized as follows: the first column reports the name of
    the patterns and it is followed by two groups of three columns
    denoted with the scope type: the first group refers to the intended
    specification, the second to the one with fault injections.
    Each cell in the first
    group reports the number of requirements grouped by pattern and by
    scope type. Cells in the second group categorize the 6 injected
    faults, labeled with F1, \ldots, F6.
  }
\end{table}

In this case study, constrained numerical signals are used to
represent requirements related to various parameters, namely
angle, speed, acceleration, and torque of the 4 joints,
size of the object picked, and force exerted by the end-effector.
We consider 75 requirements, including those involving
scenario-independent constraints like joints limits,
and mutual exclusion among states, as well as specific requirements
related to the conditions to be met at each state. The set of
requirements involved in our analysis includes 14 Boolean signals and
20 numerical ones. The full list of requirements is available
at~\cite{robotArmUsecase}, each one of them expressed as a
PSP($\mathcal{D}$). In Table~\ref{tab:robot-req} we present a synopsis
  of the requirements, to give an idea of the kind of patterns used in
  the specification.

Our first experiment\footnote{Experiments
herein presented ran on a PC equipped with a CPU Intel Core i7-2760QM @
2.40GHz (8 cores) and 8GB of RAM, running Ubuntu 14.04 LTS.}
is to run \textsc{NuSMV-invar}{} on the intended specification translated to
LTL($\mathcal{D}_C$). The motivation for presenting the results
with \textsc{NuSMV-invar}{} rather than \textsc{aalta}{} is twofold: While its performances
are worse than \textsc{aalta}{}, \textsc{NuSMV-invar}{} is more robust in the sense that it
either reaches the time limit or it solves the problem, without ever
failing for unspecified reasons like \textsc{aalta}{} does at times; second, it
turns out that \textsc{NuSMV-invar}{} can deal flawlessly and in reasonable CPU times
with all the
specifications we consider in this Section, both the intended one and
the ones obtained by injecting faults. In particular, on the intended
specification, \textsc{NuSMV-invar}{} is able to find a counterexample in 37.1 CPU
seconds, meaning that there exists at least a model able to
satisfy all the requirements simultaneously. Notice that the
translation time from patterns to formulas in LTL($\mathcal{D}_C$) is
negligible with respect to the solving time.
Our second experiment is to run \textsc{NuSMV-invar}{} on the specification with
some faults injected. In particular, we consider six different
faults, and we extend the specification in six different ways
considering one fault at a time. The patterns related to the faults
are summarized in Table~\ref{tab:robot-req}. Also in this case, we
refer the reader to~\cite{robotArmUsecase} for details.
In case of faulty specifications, \textsc{NuSMV-invar}{} concludes that no
counterexample exists, i..e, there is no model able to satisfy all the
requirements simultaneously.  In particular, in the case of
F2 and F3, \textsc{NuSMV-invar}{} returned the result in 2.1 and 1.7 CPU seconds,
respectively. Concerning the other faults, the tools was one order of
magnitude slower in returning the satisfiability result. In
particular, it spent 16.8, 50.4, 12.2, and 25.6 CPU seconds in the
evaluation of the requirements when faults 1, 4, 5 and 6 are injected,
respectively.

The noticeable difference in performances when checking for different
faults in the specification is mainly due to the fact that F2 and F3
introduce an initial inconsistency, i.e., it would not be possible to
initialize the system if they were present in the specification,
whereas the remaining faults introduce inconsistencies related to
interplay among constrains in time, and  thus additional search is
needed to spot problems. In order to explain this difference, let
us first consider fault 2:
\begin{center}
  \parbox{0.7\textwidth}{
  \emph{Globally, it is always the case that if} \texttt{state\_init}
  \emph{holds, then not } \texttt{arm\_idle} \emph{ holds as well.}
  }
\end{center}
It turns out that in the intended specification there
is one requirement specifying exactly the opposite, i.e.,
that when the robot is in \texttt{state\_init}, then \texttt{arm\_idle}
must hold as well. Thus, the only models that satisfy both requirements
are the ones preventing the robot arm to be in
\texttt{state\_init}. However, this is not possible because other
requirements related to the state evolution of the system impose that
\texttt{state\_init} will eventually occur and, in particular, that it
should be the first one.
On the other hand, if we consider fault 6:
\begin{center}
  \parbox{0.7\textwidth}{
{\it Globally, it is always the case that if} \texttt{arm\_moving}
{\it holds, then} \texttt{joint1\_speed} $>$ {\it 15.5 holds as
  well.}\\ {\it Globally,} \texttt{arm\_moving} {\it and}
\texttt{proximity\_sensor} {\it = 10.0 eventually holds.}
}
\end{center}
we can see that the first requirement sets a lower speed bound at 15.5
$deg/s$ for \texttt{joint1} when the arm is moving, while there
exists a requirement in the intended specification setting an upper
speed bound at 10 $deg/s$ when the proximity sensor detects an object
closer than 20 $cm$. In this case, the model checker is still able to
find a valid model in which \texttt{proximity\_sensor} $<$ 20.0 never
happens when \texttt{arm\_moving} holds, but the second requirements
in fault 6 prohibits this opportunity. It is exactly this kind of
interplay among different temporal properties which makes \textsc{NuSMV-invar}{}
slower in assessing the (in)consistency of some specifications.

\section{Introduction}
In the context of safety- and security-critical cyber-physical systems
(CPSs), checking  the consistency of functional requirements is an
indisputable, yet challenging task. Requirements written in natural
language call for time-consuming and error-prone manual reviews,
whereas enabling automated consistency verification often requires
overburdening formalizations. Given the increasing pervasiveness of
CPSs, their stringent time-to-market and product budget constraints,
practical solutions to enable automated verification of requirements
are in order, and
Property Specification Patterns (PSPs)~\cite{dwyer1999} offer a viable
path towards this target.
PSPs are a collection of parameterizable, high-level,
formalism-independent specification abstractions, originally developed
to capture recurring solutions to the needs of requirement engineering.
Each pattern can be directly encoded in a formal specification
language, such as linear time temporal logic (LTL)~\cite{pnueli1992},
computational tree logic (CTL)~\cite{clarke1986}, or graphical
interval logic (GIL)~\cite{dillon1994}.
Because of their features, PSPs may ease the burden of formalizing
requirements, yet enable their verification using current
state-of-the-art automated reasoning tools --- see,
e.g.,~\cite{li2013,li2013b,schwendimann1998,cimatti2002,hustadt2003}.

The original formulation of PSPs caters for temporal structure over
Boolean variables. However, for most practical applications, such
expressiveness is too restricted. This is the case of the embedded
controller for robotic manipulators that is under development in the
context of the EU project CERBERO\footnote{Cross-layer modEl-based
  fRamework for multi-oBjective dEsign of Reconfigurable systems in
  unceRtain hybRid envirOnments ---
  \url{http://www.cerbero-h2020.eu/}} and provides the main motivation
for this work. As an example, consider the following statement:
``\textit{The angle of joint1 shall never be greater than 170
  degrees}''. This requirement imposes a safety threshold related to
some joint of the manipulator (\textit{joint1}) with respect to
physically-realizable poses, yet it cannot be expressed as a PSP
unless we add atomic assertions from a constraint system
$\mathcal{D}$.  We call Constraint PSP, or PSP($\mathcal{D}$) for
short, a pattern which has the same structure of a PSP, but contains
atomic propositions from $\mathcal{D}$. For instance, using
PSP($\mathbb{R},<,=$) we can rewrite the above requirement as an
\textit{universality} pattern: ``\textsl{Globally, it is always the
  case that $\theta_1 < 170$ holds}'', where $\theta_1$ is the
numerical signal (variable) for the angle of \textit{joint1}.  In
principle, automated reasoning about Constraint PSPs can be performed
in Constraint Linear Temporal Logic, i.e., LTL extended with atomic
assertions from a constraint system~\cite{demri2002}: in our example
above, the encoding would be simply $\Box(\theta_1 < 170)$.
Unfortunately, this approach does not always lend itself to a
practical solution, because Constraint Linear Temporal Logic
is undecidable in
general~\cite{comon2000}. Restrictions on $\mathcal{D}$ may restore
decidability~\cite{demri2002}, but they introduce limitations
in the expressiveness of the corresponding PSPs.

In this paper, we propose a solution which ensures that automated
verification of requirements is feasible, yet enables PSPs mixing
both Boolean variables and (constrained) numerical signals. Our approach
enables us to capture many specifications of practical interest,
and to pick a verification procedure from the relatively
large pool of automated reasoning systems currently available for LTL.
In particular, we restrict our attention to a constraint systems of the
form ($\mathbb{R}$,$<$,$=$), and atomic propositions of the form
$x < C$ or $x = C$, where $x \in \mathbb{R}$ is a variable
and $C \in \mathbb{R}$ is a constant value. In the following,
we write $\mathcal{D}_C$ to denote such restriction. Our contribution
can be summarized as follows:
\begin{itemize}
\item We extended basic PSPs over the constraint system
  $\mathcal{D}_C$, and we provided an encoding from any
  PSP($\mathcal{D}_C$) into a corresponding LTL formula.
\item We implemented a generator of artificial requirements expressed
  as PSPs($\mathcal{D}_C$); the generator has a number of parameters,
  and it uses a probability model to choose
  the specific pattern to emit.
\item Using our generator, we ran an extensive experimental evaluation
  aimed at understanding $(i)$ which automated reasoning tool is best
  at handling set of requirements as PSPs($\mathcal{D}_C$), and $(ii)$
  whether our approach is scalable.
\item Finally, we analyzed the requirements of the aforementioned
  embedded controller, experimenting also with the addition of faulty
  ones.
\end{itemize}
The consistency of requirements written in PSP($\mathcal{D}_C$) is
carried out using tools and techniques available in the
literature~\cite{rozier2010,rozier2011,panda,li2013b}. With those,
we demonstrate the scalability of our approach by checking the
consistency of up to 1920 requirements, featuring 160 variables and
domains of size 8 within less than 500 CPU seconds.
A total of 75 requirements about the embedded controller for the
CERBERO project is checked in a matter of seconds, even without
resorting to the best tool among those we consider.

The rest of the paper is organized as
follows. Section~\ref{sec:background} contains some basic concepts on
LTL, PSPs and some related work. In Section~\ref{sec:consistency} we
present the extension of basic PSPs over $\mathcal{D}_C$ and the
related encoding to LTL. In Sections~\ref{sec:random}
and~\ref{sec:robot} we report the results of the experimental analysis
concerning the scalability and the case study on the embedded
controller, respectively. We conclude the paper in
Section~\ref{sec:concl} with some final remarks.

\input{background}
\input{signal}
\input{exp-random}
\input{exp-robot}

\section{Conclusions}
\label{sec:concl}
Enabling the verification of high-level requirements is one of the key
aspects towards the development of safety- and security-critical
cyber-physical systems.
Property Specification Patterns offer a viable path towards
this target, but their expressiveness is often too restricted for
practical applications.
In this paper, we have extended basic PSPs over the constraint system
$\mathcal{D}_C$, and we have provided an encoding from any
PSP($\mathcal{D}_C$) into a corresponding LTL formula.
This enables us to deal with many specifications of practical interest,
and to verify them using  automated reasoning systems currently
available for LTL.
Using realistically-sized specifications generated with an artificial
probability model we have shown that our approach implemented on the
tool \textsc{aalta}{} scales to problems containing more than a thousand
requirements over hundreds of variables. Considering a real-world case
study in the context of the EU project CERBERO, we have shown
that it is feasible to check specifications and uncover injected
faults, even without resorting to \textsc{aalta}{}, but considering the
(slower, yet more robust) \textsc{NuSMV}. These results witness that our
approach is viable and worth of adoption in the process of requirement
engineering.  Our next steps toward this goal will include easing the
translation from natural language requirements to patterns, and
extending the pattern language to deal with other relevant aspects of
cyber-physical systems, e.g., real-time constraints.

\paragraph{Acknowledgments} The research of Luca Pulina and Simone Vuotto has been funded by the EU Commission's H2020 Programme under grant agreement N. 732105 (CERBERO project).

\bibliographystyle{splncs03}

\section{Constraint Property Specification Patterns}
\label{sec:consistency}

Let us start by defining a \emph{constraint systems} $\mathcal{D}$
as a tuple $\mathcal{D} = (D, R_1, \ldots, R_n, \mathcal{I}$), where
$D$ is a non-empty set called \emph{domain}, and each
$R_i$ is a predicate symbol of arity $a_i$, with
$\mathcal{I}$($R_i)$ $\subseteq$ $D^{a_i}$ being its
interpretation. An (atomic) $\mathcal{D}$-\emph{constraint} over a set of
variables $X$  is of the form $R_i(x_1, \ldots, x_{a_i})$ for some
$1 \leq i \leq n$ and $x_j \in X$ for all $1 \leq j \leq a_i$ --- we
also use the term
\emph{constraint} when $\mathcal{D}$ is understood from the context.
We define \emph{linear temporal logic modulo constraints}
--- LTL($\mathcal{D}$) for short --- as an extension of LTL with atoms
in a constraint system $\mathcal{D}$. Given a set of Boolean
propositions $Prop$, a constraint system $\mathcal{D} = (D, R_1,
\ldots, R_n, \mathcal{I})$, and a set of variables $X$, an
LTL($\mathcal{D}$) formula is defined as:
\begin{center}
  $\phi =$ $\bot$ $\mid$ $\top$ $\mid$ $p$ $\mid$ $R_i(x_1, \ldots,
  x_{a_i})$ $\mid$ $\neg \phi_1$
  $\mid$ $\phi_1\vee\phi_2$ $\mid$ $\mathcal{X}
  \phi_1$ $\mid$ $\phi_1 \mathcal{U} \phi_2$
\end{center}
where $p \in Prop$, $\phi, \phi_1, \phi_2$ are LTL($\mathcal{D}$)
formulas,  and $R_i(\cdot)$ with $1 \leq i \leq n$ is an atomic
$\mathcal{D}$-constraint. Additional Boolean and temporal operators
are defined as in LTL with the same intended
meaning. Notice that the set of LTL($\mathcal{D}$) formulas is a
(strict) subset of those in constraint linear temporal logic ---
CLTL($\mathcal{D}$) for short --- as defined, e.g.,
in~\cite{demri2002}. LTL($\mathcal{D}$) formulas are also interpreted
over computations of the form $\pi: \mathbb{N} \rightarrow 2^{Prop}$
plus additional \emph{evaluations} of the form $\nu: X \times
\mathbb{N} \rightarrow D$, i.e., $\nu$ is a function assigning at
each variable $x \in X$ a corresponding value $\nu(x,i)$
at each time instant $i \in \mathbb{N}$. LTL semantics is extended to
LTL($\mathcal{D}$) by handling constraints:
\begin{center}
  $\pi,\nu,j \models R_i(x_1, \ldots, x_{a_i})$ iff
  $(\nu(x_1,j), \ldots, \nu(x_{a_i},j)) \in \mathcal{I}(R_i)$
\end{center}
We say that $\pi$ and $\nu$ \emph{satisfy} a formula $\phi$, denoted
$\pi, \nu \models \phi$, iff $\pi, \nu, 0 \models \phi$. A formula
$\phi$ is \emph{satisfiable} as long as there exist a computation
$\pi$ and a valuation $\nu$ such that $\pi, \nu \models \phi$.
We further restrict our attention to the constraint system $D_C$ =
($\mathbb{R}$,$<$,$=$), with atomic constraints of the form $x < C$
and $x = C$, where $C \in \mathbb{R}$ is a constant.
While CLTL($\mathcal{D}$) is undecidable in
general~\cite{demri2002,comon2000}, LTL$(\mathcal{D}_C)$ is decidable
since, as we show in the following, it can be reduced to LTL satisfiability.

We introduce the concept of \emph{constraint property specification
  pattern}, denoted PSP($\mathcal{D}$), to deal with specifications
containing Boolean variables as well as atoms from a constraint system
$\mathcal{D}$. In particular, a PSP($\mathcal{D}_C$) features only
Boolean atoms and atomic constraints of the form
$x < C$ or $x = C$ ($C \in \mathbb{R}$). For example, the requirement:
\begin{center}
  \emph{The angle of joint1 shall never be greater than 170 degrees}
\end{center}
can be re-written as a PSP($\mathcal{D}_C$):
\begin{center}
  \emph{Globally, it is always the case that $\theta_1 < 170$}
\end{center}
where $\theta_1 \in \mathbb{R}$ is the variable associated to the
angle of \emph{joint1} and $170$ is the limiting threshold.
While basic PSPs only allow for Boolean states/events in
their description, PSPs($\mathcal{D}_C$) also allow for atomic
constraints. It is straightforward to extend the translation
of~\cite{dwyer1999} from basic PSPs to LTL in order to encode any
PSP($\mathcal{D}_C$) to a formula in LTL($\mathcal{D}_C$). Consider,
for instance, the set of requirements:
\begin{itemize}
\item[$R_1$] Globally, it is always the case that \textbf{v $\leq$
  5.0} holds.
\item[$R_2$] After \textbf{a}, \textbf{v $\leq$ 8.5} eventually holds.
\item[$R_3$] After \textbf{a}, it is always the case that if
  \textbf{v $\geq$ 3.2} holds, then \textbf{z} eventually holds.
\end{itemize}
where \textbf{a} and \textbf{z} are Boolean states/events, whereas
\textbf{v} is a numeric signal.
These PSPs($\mathcal{D}_C$)\footnote{Strictly speaking, the syntax
  used is not that of $\mathcal{D}_C$, but a statement like $v \leq
  5.0$ can be thought as syntactic sugar for the expression $(v <
  5.0) \vee (v = 5.0)$.}
can be rewritten as the following LTL($\mathcal{D}_C$) formula:
\begin{equation}
  \label{eq:reqex}
  \begin{array}{ll}
    \Box (v < 5.0 \vee v = 5.0) & \wedge \\
    \Box (a \rightarrow \Diamond (v < 8.5) \vee (v = 8.5)) & \wedge \\
    \Box (a \rightarrow \Box (\neg (v < 3.2) \rightarrow \Diamond z))
  \end{array}
\end{equation}
Therefore, to reason about the consistency of sets of requirements
written using PSPs($\mathcal{D}_C$) it is sufficient to provide an
algorithm for deciding the satisfiability of LTL($\mathcal{D}_C$)
formulas.

To this end, consider an LTL($\mathcal{D}_C$) formula $\phi$, and
let $X(\phi)$ be the set of variables that occur in $\phi$.
We define the \emph{set of thresholds} $T_x(\phi)$ as the set of
constant values against which variable $x \in X(\phi)$ is compared to.
More precisely, for every variable $x \in X(\phi)$ we construct a
set $T_x(\phi)$ = $\{t_1,..,t_n\}$ such that, for all $t_i \in
\mathbb{R}$ with $1 \leq i \leq n$, $\phi$ contains a constraint of
the form $x < t_i$ or $x = t_i$. In the following, for our
convenience, we consider each threshold set $T_x(\phi)$ ordered in
ascending order, i.e., $t_{i} < t_{i+1}$ for all $1 \leq i < n$. For
instance, in example (\ref{eq:reqex}), we have $X = \{v \}$ and the set
$T_v = \{ 3.2, 5.0, 8.5 \}$. Given an LTL($\mathcal{D}$) formula
$\phi$, let $T_x(\phi) = \{t_1, \ldots, t_n \}$ be the ordered set of
thresholds for some variable $x \in X(\phi)$; given a computation
$\pi$ and a valuation $\nu$ we can define:
\begin{itemize}
\item $C_x(\phi)$ as the set of Boolean variables such that for each
  $c_j \in C_x(\phi)$ we have $c_j \in \pi(i)$ for $i = 0, 1, \ldots$
  exactly when $t_{j-1} < \nu(x,i) < t_j$, if $j >1$, and $\nu(x,i) <
  t_j$, if $j = 1$  with $t_j \in T_x(\phi)$ for all $1 \leq j \leq n$.
\item $E_x(\phi)$ as the set of Boolean variables such that
  for each $e_j \in E_x(\phi)$ we have $e_j \in \pi(i)$ for $i = 0, 1,
  \ldots$ exactly when $\nu(x,i) = t_j$ for some $t_j \in T_x(\phi)$.
\end{itemize}
Notice that, by definition of $C_x(\phi)$ and $E_x(\phi$), given any
time instant $i \in 0, 1, 2, \ldots$, we have that exactly
one of the following cases is true ($1 \leq j \leq n$):
\begin{itemize}
  \item $c_j \in \pi(i)$ for some $j$, $c_l \not\in
    \pi(i)$ for all $l \neq j$ and  $e_j \not\in \pi(i)$ for all $j$;
  \item $e_j \in \pi(i)$ for some $j$, $e_l \not\in
    \pi(i)$ for all $l \neq j$ and  $c_j \not\in \pi(i)$ for all $j$;
  \item $c_j \not\in \pi(i)$ and $e_j \not\in \pi(i)$ for all $j$.
\end{itemize}
Intuitively, the first case above corresponds to a value
of $x$ that lies between some threshold value in
$T_x(\phi)$ or before its smallest value; the second case occurs
when a threshold value is assigned to $x$, and the third case is when
$x$ exceeds the highest threshold value in $T_x(\phi)$.
For instance, in example (\ref{eq:reqex}) we have
$T_v = \{ 3.2,  5.0, 8.5 \}$ and the corresponding sets
$C_v \{c_1, c_2, c_3 \}$ and $E_v = \{e_1, e_2 ,e_3\}$. Assuming,
e.g., $\nu(v,i) = 10$ for some $i = 0, 1, 2, \ldots$, we would have
that $C_v \cap \pi(i) = E_v \cap \pi(i) = \emptyset$.

Given the definitions above, an LTL($\mathcal{D}$) formula $\phi$ over the
set of Boolean propositions $Prop$ and the set of variables $X$, can be
converted to an LTL formula $\phi'$ over the set of Boolean
propositions $Prop \cup \bigcup_{\xi in X} (C_\xi(\phi) \cup E_\xi(\phi))$ using the following
substitutions:
\begin{equation}
  \label{eq:encoding}
  x < t_i \leadsto \bigvee_{j=1}^i c_j \vee \bigvee_{j=1}^{i-1}e_j
  \qquad \mbox{and} \qquad
    x = t_i \leadsto e_j.
\end{equation}
However, replacing atomic constraints is not enough to ensure
equisatisfiability of $\phi'$ with respect to $\phi$. In particular,
we must encode the observation made above about ``mutually exclusive''
Boolean valuations for variables in $C_x(\phi)$ and $E_x(\phi)$ for
every $x \in X(\phi)$ as corresponding Boolean constraints:
\begin{equation}
  \label{eq:phiM}
    \phi_M = \bigwedge_{\xi \in X(\phi)} \left( \bigwedge_{a,b \in M_{\xi(\phi)}, a \neq
    b} \Box \neg (a \wedge b) \right)
\end{equation}
where $M_\xi(\phi) = C_\xi(\phi) \cup E_\xi(\phi)$. We can now state
the following fact:
\begin{property}
  \label{prop:key}
Given an LTL($\mathcal{D}_C$) formula $\phi$ over the set of Boolean
atoms $Prop$ and variables $X(\phi)$, and the corresponding sets
$C_x(\phi)$ and $E_x(\phi)$ defined for all $x \in X(\phi)$ as
described above, we have that $\phi$ is satisfiable if and only if the
LTL formula $\phi_M \rightarrow \phi'$ is satisfiable, where $\phi'$ is
obtained by replacing atomic constraints according to rules
(\ref{eq:encoding}) and $\phi_M$ is defined according to (\ref{eq:phiM}).
\end{property}
For instance, given example (\ref{eq:reqex}), we have $C_v = \{c_1,
c_2, c_3\}$ and $E_v = \{e_1, e_2, e_3\}$ and the mutual exclusion constraints
are written as:
\begin{equation}
\begin{split}
  \phi_{M} =&
  \Box \neg (c_1 \wedge c_2) \wedge \Box \neg (c_1 \wedge c_3) \wedge
  \Box \neg (c_1 \wedge e_1) \wedge \Box \neg (c_1 \wedge e_2) \wedge  \\&
  \Box \neg (c_1 \wedge e_3) \wedge \Box \neg (c_2 \wedge c_3) \wedge
  \Box \neg (c_2 \wedge e_1) \wedge \Box \neg (c_2 \wedge e_2) \wedge  \\&
  \Box \neg (c_2 \wedge e_3) \wedge \Box \neg (c_3 \wedge e_1) \wedge
  \Box \neg (c_3 \wedge e_2) \wedge \Box \neg (c_3 \wedge e_3) \wedge  \\&
  \Box \neg (e_1 \wedge e_2) \wedge \Box \neg (e_1 \wedge e_3) \wedge
  \Box \neg (e_2 \wedge e_3).
\end{split}
\end{equation}
Therefore, the LTL formula to be tested for assessing the consistency of
the requirements is
\begin{equation}
  \label{eq:reqex2}
  \begin{array}{ll}
    \phi_M \rightarrow ( & \Box (c_1 \vee c_2 \vee e_1 \vee e_2) \wedge \\
                         & \Box (a \rightarrow \Diamond (\bigvee_{i=1}^3 c_i \vee e_i)) \wedge \\
                         & \Box (a \rightarrow \Box (\neg (c_1 \vee e_1) \rightarrow \Diamond z))).
  \end{array}
\end{equation}

redpajama_set_name: RedPajamaArXiv


text:
\section{はじめに}

脳血腫は6-24時間に急成長を遂げ, 予測を誤り脳外科医が手術しなければ命を
落とす. しかし, 脳血腫には急成長をする型と急成長に至らない型の2通りが
存在し, 脳血腫か否かはCTなどによる検査を最低限必要となる. 急成長をする
型の脳血腫であることを判定するには通常の医師には難しく, 専門の脳外科医
が判定を行う必要のあるケースが多く存在する. CTは脳血腫が存在するかない
かの簡便な検査方法として広く知られており、しかも、大きい病院だけでなく,
小さな病院においても検査が可能となる. このため, われわれのターゲットと
するシナリオは, 小さな病院においてCTで撮影を行ない, このCT画像を人工知
能で分析し, もし疑わしければ, 大学病院などの脳外科の専門医に患者を運び
込むというシナリオである.

このシナリオに従って, CTでの撮像画像を与えられ, 急成長する可能性のある
血腫のどのクラスに属するかを判定するタスクを本論文では扱う.
この急発達の予測は典型的に頻度の少ない事象を学習する困難な問題となるだ
けでなく, 形状が動的な変化をしているかのようにフレキシブルな形状を取る.

本論文の構成は以下の通りである. 第2節では, 血腫の分類の歴史的なコンテ
クストと急成長のための分類法をレビューする. 第3節ではセグメンテーショ
ンと分類のジョイント学習法を提案し, 性能を評価する.
第4節では, 結論と今後の課題について述べる.

\section{関連手法}
\section{血腫分類タスク}

\subsection{血腫分類の歴史的コンテクスト}

急性脳内血腫(ICH)は脳小血管病(SVD)が発展したもので, このうち3分の1の患
者においてはさらに出血が持続する. 臨床的にこの脳内血腫の増大の可能性を
初期に検知できることは患者の治療に非常に役立つと考えられている.  脳血
腫の増大の最も単純なモデルにおいては、まず, 初期症状において小血管の一
つが血腫を形成する. 次に, 二次的な機械的な剪断損傷などを原因として出血
が持続して広がる. さらに, ヘマトクリット値と蛋白質により密度が個々のケー
スにより異なる形で凝集する. このとき, 見た目は柔組織の傷害、出血による
脳浮腫、脳室系の拡大などの隣接する構造に依存し, 呈する形状はこれらに依
存してかなり異なる. このモデルからも示唆されるように, 脳血腫の形成は以
下のような特徴をもつ.  1つ目は時系列で血腫拡大が形成されることである.
2つ目は最終的な出血の体積は周辺部の損傷した血管の個数によることである.
3つ目は拡大する方向は軸の向き通りではなく, 拡大した血腫の形状は非定型
となることである.

脳血腫の分類にはさまざまな方式が考えられてきた. 1つ目, マージンの形状
の分類を記述する初期の論文は形状の分類を題材とし, 出血の拡大の影響を直
接の題材としていないが, 後の研究により関係が報告されている. これらは以
下の3つの論文である.
\cite{Fujii94}
は脳血腫の形状による分類を試
みた.  丸形状(丸形状のスムーズなマージン), 非定型形状(非定型形状のマル
チノードのマージン), 分離した形状(定型と非定型を二分するフルイドレベル)の
3つである. \cite{Barras09}は急性脳内血腫(ICH)の形状を定型から非定
型までの5段階で分類した.  \cite{Blacquiere15}は同じスケールを用い
て, 非定型なマージンと出血の拡大は独立な関係にあることを考察した. 2つ
目, 血腫拡大がヘテロな出血から来ることを示唆する最初の率直な証拠は,
\cite{Kim08}のスワールサインの分類による. 3つ目, \cite{Li16}
はスワールサインにさらなる条件を課し, ブラックホールサインを
定義した.  このブラックホールサインは高い特異値において出血拡大に関係
していることを示した.

本論文においては, 出血拡大に関係性が高いと考えら
れるハイポデンシティー(hypodensities), マージンイレギュラーサイン
(margin irregularity), ブレンドサイン(blend sign), フルイドレベル
(fluid levels)の4つのクラスに対して分類を行なう\cite{Boulouis16}.

\subsection{ICH拡張に焦点を絞った血腫分類}

図2はBoulouisら\cite{Boulouis16}の以下の4つのクラスへの分類を示す.
  \begin{itemize}
  \item A: ハイポデンシティー(hypodensities, swirl sign/black hole sign/central hypodensity)
  \item B: マージンイレギュラーサイン(Intracerebral hemorrhage with irregular margins and ICH with heterogeneous densities)
  \item C: ブレンドサイン
    \item D: フルイドレベル
  \end{itemize}
この分類に従って血腫分類タスクを上記4つのクラスに分類するタスクとして
考える.  つまり, 与えられた時刻$t$における患者$h_i$の脳CT画像列に対し
て, ハイポデンシティー, マージンイレギュラーサイン, ブレンドサイン, フ
ルイドレベルの4つのクラスに対して分類を行なうタスクである.

血腫をこれら4クラスに分類をするBoulouisらの目的の一つは, これらのそれ
ぞれの血腫の分類の型のICHの拡張率の違いである. つまり, ハイポデンシ
ティー: 20.2\%, マージンイレギュラーサイン: 14.0\%, ブレンドサイン:
35\%, フルイドレベル: (記述なし)という拡張率となるからである.  なお,
これらの4クラスは重複可能である. 血腫は複数のクラスに同時に属するモデ
ルを考え,各々のクラスを独立とみなし二値分類問題と考える. つまりマルチ
クラスの分類ではない.

ハイポデンシティー(図3参照)は出血の中にハイポデンスな構造が存在することを総称す
る. 具体的にはスワールサイン, ブラックホールサイン, ヘテロな密度スケー
ル(density heterogeneity scale)という, いずれも同じ現象を捉えていると
考えられているサインがあるかないかで判断される. スワールサインは飲み込
むような見え方,ブラックホールサインはブラックホールが中心に存在するか
のような見え方,ヘテロな密度スケールはヘテロな出血かホモジニアスな出血
かを1から5までのスケールで評価する指標をさす.

ブレンドサイン\cite{Li16}は血腫の中に, ハイパーアテニュエイトな領域と
隣接するハイパーアテニュエイトな領域が混ざったものをいう. 17\%の患者か
ら, このブレンドサインの存在は出血拡大を示唆するという報告もある.

マージンイレギュラーサインは,出血の形状が丸型の形状や分離した形状では
なく非定型な形状をいう\cite{Fujii94}. このサインは出血が成熟して
いないことを視覚的に捉えながら, 周辺部における血腫の境界における二次的
な出血に影響されている可能性はある.

ハイポデンシティーは球状で, 中心が一つで, その形状で一度だけ拡張して収
縮する. 中心に黒い点(ブラックホール)があれば, 拡張率は高い. イレギュラー
マージンの形状は(複数の中心を持ち)丸ではなく, 若干ひしゃげている. ブレ
ンドサインはハイポデンシティーと類似するが, 形状は若干小さく, 白みがかっ
ている. 拡張率は高い. フルイドレベルは血腫が(黒みがかって)液状化する図
となる.

なお、血腫の形状は実際には3D空間にこれが存在する. このため, 血腫の形状
が球である場合, CT画像で丸であることと同時にCT画像と直行する方向におい
ても, 球程度である必要がある.

また, それぞれ4種類の分類は排他的関係にある. つまり重複を許す.  したがっ
て,目標としては, これらの重複を考慮したクラスを増設した. つまり, CT画
像において, ハイポデンシティーとブレンドサインの両方に当て嵌るクラスで
あれば, これをクラスとして設定した. このやり方で用いて分類すると, ほと
んどのブレンドサインのみ, フルイドレベルのみという分類は非常に少なく,
大半のCT画像は他のクラスとの混合クラス、もしくは, 血腫なしという分類と
なる. ただ、血腫の形状がハイポデンシティーが球状で, マージンイレギュラー
サインが楕円状であるという違いからこれらが同時に起こるというのはあまり
ない.

\subsection{血腫ICH拡張タスク}

ICHが拡大するか否かは, 現実的な問題として非常に重要である. また,脳血腫
にはIVHという指標も関係するが, 本論文ではCT撮影時の体積を測定し, それ
に基づいた時間間隔において, ICHが30\%以上拡大したか否かを判定する. 他
に30ml以上増加したなどが議論されることもあるが, ここではICH30\%以上の
拡大のみを論ずる.

このプロトコルはいくつかの機械学習的な困難さを伴う.  1つ目, この間隔は
実際の患者の撮影条件によるため, まちまちである. これは正確には時間ごと
に変化するはずだが, ここではこれを議論しない. これを突き詰めると欠損値
問題になるが, ここでは単純な教師あり学習として扱う. 2つ目, ICH30\%以上
拡大するか否かという2値分類のみの形で論ずる. 3つ目, 本来, 個体毎にICH
が30\%以上拡張するか否かということを議論しているが, スライスで見た場合
にはあるスライスではICH30\%以上するかもしれないが, 他のスライスでは拡
張する必要はない. 画像のみの情報に基づき拡張性を議論する場合, スライス
に拡張があるかないかはどちらかといえば, ないように思える. 血腫はある部
位で異常が起こったとしても, その部位以外の所で起こる事象とは独立であること
が多いと考えられる. 一方, 血腫がある場合, その血腫が一定時間後に拡張する
かどうかは画像内に表われる可能性がある.

\section{手法}

\subsection{データセットと前処理}

CTスキャンは、12の施設から収集した。各被験者の情報は匿名化した。CTスキャンにおける血腫の範囲や位置、状態などのアノテーションは、12の施設の専門医でそれぞれ別で行われた。

CTスキャンのスライス画像のサイズは、512$\times$512である。CTスキャンのデータは、DICOM形式で保存されており、ピクセル値の単位はハウンズフィールド単位(HU)である。1つ目の前処理として、式\ref{equa:hu}のように、対象のHU範囲を選択してコントラストを調整した。

\begin{equation}
    \label{equa:hu}
    I(i,j) =
    \begin{cases}
    0 & if I_{HU}(i,j) < a\\
    \frac{I_{HU}(i,j)-a}{b-a} \times 255 & if a \leq I_{HU}(i,j) \leq b\\
    255 & if I_{HU}(i,j) > b
    \end{cases}
\end{equation}

ここで、$I(x)$は、位置$x$でのコントラスト調整後の強度である。$a=0$と$b=80$は、脳のCT画像を可視化するために一般的に使用される。本研究では、CTスキャンを収集したそれぞれの施設の専門医が決定したパラメータ$a$,$b$を用いており、おおよそ$a=0$と$b=80$であった。

さらに、CT画像の前処理の記事(\url{https://vincentblog.xyz/posts/medical-images-in-python-computed-tomography})に従って、ノイズ除去、骨除去、中央への位置合わせの前処理を行った。ノイズ除去では、CTスキャンの際に映るアーイファクトを除去した。骨除去では、頭蓋骨部分を除去した。これは、コントラスト調整後のCT画像において骨の部分が白く映り、情報が強くなる(白は最大のピクセル値255)と考えたためである。中央への位置合わせでは、脳を画像の中央に平行移動する作業を行った。

\subsection{セグメンテーションと分類のためのジョイントモデル}

図\ref{fig:model}は、本研究で提案するセグメンテーションと分類のためのジョイントモデルのアーキテクチャを示している。提案するモデルは、1つのモデルでセグメンテーションと分類の2つのタスクを行う。具体的に、U-Net(図\ref{fig:model}の上のパス)でセグメンテーションのタスクを行い、Wavelet CNN(図\ref{fig:model}の下のパス)で分類のタスクを行う。ここで分類のタスクでは、U-Netのエンコーダより得られる特徴と、Wavelet CNNより得られる特徴の2つを用いて分類を行う。提案するモデルへの入力は前処理後の2DのCT画像であり、セグメンテーションタスクの出力は確率マップ([0,1])、分類タスクの出力は確率ベクトル([0,1])である。ここで、確率マップの各位置の値は対応するピクセルが属する確率を示す(血腫領域の場合は1、それ以外は0)。確率ベクトルの各要素の値は、対応する血腫状態である確率を示す。

\vspace{1cm}
\begin{figure}[h]

\includegraphics[width=60mm]{model.png}
\caption{
提案するセグメンテーションと分類のためのジョイントモデルのアーキテクチャ
}
\label{fig:model}
\end{figure}

\subsubsection*{U-Net}
血腫領域のセグメンテーションタスクには、エンコーダ/デーコーダ構造のCNNを採用している。ダウンサンプリングのエンコーダには、Efficientnet-b3モデルを用いている。また、U-Netに従い、エンコーダとデーコーダの対応するレイヤ間にスキップ接続を追加している。

\subsubsection*{Wavelet CNN}
血腫にはテスチャにも情報を持っている。そのため、血腫状態の分類タスクには、一般的なCNNではなく、Wavelet CNNを採用している。Wavelet CNNの中心的なアイデアは、ウェーブレット変換をCNNアーキテクチャに組み込んで、画像のテクスチャ情報を保持することである。一般的なCNNでは、受容野を拡大するために用いられるプーリング処理の際に、エッジ情報が保持され、テクスチャ情報は損失する可能性がある。本研究では、VGG16モデルのプーリング層をウェーブレット変換に変更したCNNをWavelet CNNとして扱う。

\subsubsection*{マルチラベルの分類}
血腫状態の分類タスクは、各CT画像が1つずつのクラスに属する多クラス分類ではなく、いくつかのクラスに属するマルチラベルの分類タスクである。一般的な多クラス分類では、出力層の活性化関数としてsoftmax関数を用いる。一方で、マルチラベルの分類タスクではsigmoid関数を用いる。これは明確で、softmax関数の定義が、sigmoidの和で割ったものだからである。softmax関数の出力$y_i$の合計は必ず1になるが、sigmoid関数の出力$y_i$の合計が1になる保証はない。sigmoid関数の出力$y_i$は、$y_i$のそれぞれが[0,1]の範囲の値になる。

また、一般的な多クラス分類では損失関数として多クラス交差エントロピーを用いることが多い。一方で、マルチラベルの分類では二値交差エントロピーを用いる。本研究では、血腫状態のラベル分布が不均衡なため、式\ref{equa:loss}のような重み付きの二値交差エントロピーを用いる。

\begin{equation}
    \begin{split}
    \label{equa:loss}
    & L(x,y) = \\
    & - \frac{1}{NC} \sum_{n=1}^{N} \sum_{c=1}^{C} [w_c y_{n,c} \cdot log(x_{n,c}) \\
    & + (1-y_{n,c}) \cdot log(1-x_{n,c})] \\
    & weight(c) = \frac{sum(negative examples(c))}{sum(positive examples(c))}
    \end{split}
\end{equation}

\subsubsection*{学習手順}
提案するモデルは、2段階の学習手順を採用している。第1段階では、セグメンテーションを行うU-Netを学習する。第2段階では、分類を行うWavelet CNNを学習する。この際、U-Netのエンコーダより得られる特徴も使用するが、U-Netの重みは固定している。

\section{実験}

\subsection{血腫領域のセグメンテーション}
\subsubsection{データセットの分割方法や前処理の影響}

データセットの分割方法や前処理の影響を評価した。CT画像を訓練用とテスト用に分割する方法として、ランダムに分割する場合と、患者ごとに分割する場合の2つを考えた。
また、CT画像の前処理がセグメンテーションの精度に対してどのような影響を与えるのかを評価した。

データセットを患者ごとに分割する場合よりも、ランダムに分割した場合の方が精度が低かった(表x)。この結果は、ランダムに分割した場合には、訓練データセットとテストデータセット間で似た画像が含まれる可能性があるためである。つまり、ランダムに分割すると同じ患者から得られる複数枚のスライス画像が、訓練データセットとテストデータセットに含まれる可能性がある。また、CT画像の前処理を行うことで、精度が向上することを確認した(表x)。

\begin{table}[h]
\begin{tabular}{|l|l|l|l|}
\hline
                                                                     & dice loss & iou    & fscore \\ \hline
ランダム分割                                                               & 0.1367    & 0.7809 & 0.8633 \\ \hline
患者分割                                                                 & 0.1609    & 0.7573 & 0.8390 \\ \hline
\begin{tabular}[c]{@{}l@{}}患者分割\\ + ノイズ除去\\ + 骨除去\\ + 中央への位置合わせ\end{tabular} & 0.1464    & 0.7660 & 0.8536 \\ \hline
\end{tabular}
\end{table}

\subsubsection{血腫位置を考慮した学習}

血腫の位置を考慮してモデルを学習させることで、精度が向上するのかを評価した。具体的には、まず初めに、血腫の位置を考慮せずにモデルの学習を行い学習済みモデルを作成する。その後、血腫の位置xのデータセットのみを用いて、学習済みモデルをファインチューニングさせる。データセットは患者ごとで分割を行い、前処理は行なっていない。

血腫の位置に従ってファインチューニングを行なったが、精度の向上は見られなかった。具体的には、血腫の位置を考慮せずに学習を行なったモデルの、「位置a. 被殻」のデータセットに対する精度は0.9094であり、「位置a. 被殻」のデータセットのみを用いてファインチューニングを行なったが、精度は0.88904と低下した。同様に他の血腫の位置についても、ファインチューニングを行うことによる精度の向上は見られなかった。

\begin{table}[h]
\begin{tabular}{|l|l|l|l|}
\hline
条件                                                                & \begin{tabular}[c]{@{}l@{}}位置a.\\ 被殻\end{tabular} & \begin{tabular}[c]{@{}l@{}}位置b.\\ 視床\end{tabular} & \begin{tabular}[c]{@{}l@{}}位置c.\\ 皮質下\end{tabular} \\ \hline
全データで学習                                                           & 0.9094                                            & 0.8524                                            & 0.8726                                             \\ \hline
\begin{tabular}[c]{@{}l@{}}位置a. 被殻に従って\\ ファインチューニング\end{tabular}  & 0.8904                                            &                                                   &                                                    \\ \hline
\begin{tabular}[c]{@{}l@{}}位置b. 視床に従って\\ ファインチューニング\end{tabular}  &                                                   & 0.8364                                            &                                                    \\ \hline
\begin{tabular}[c]{@{}l@{}}位置c. 皮質下に従って\\ ファインチューニング\end{tabular} &                                                   &                                                   & 0.8607                                             \\ \hline
\end{tabular}
\end{table}

\subsection{血腫状態の分類}

\subsubsection{Wavelet CNNの影響}
Wavelet CNNによって分類の精度が向上するかを評価した。データセットは12つの施設から得られたCT画像を用い、患者ごとに訓練用とテスト用に分割した。データセットの前処理は行っていない。ジョイントモデルの条件として次の4つを考慮した;1. VGG16、2. 重み付き損失のVGG16、3. Wavelet VGG16、4. 重み付き損失のWavelet VGG16。結果として、重み付きwavelet vgg16の場合、特にhypodensityやirregularで高いaucが得られた(表xxx)。

\begin{table}[h]
\begin{tabular}{|l|l|l|l|}
\hline
条件                & hypodensity & irregular & blend \\ \hline
vgg16             & 0.692       & 0.337     & 0.524 \\ \hline
重み付きvgg16         & 0.699       & 0.471     & 0.545 \\ \hline
wavelet vgg16     & 0.650       & 0.608     & 0.613 \\ \hline
重み付きwavelet vgg16 & 0.702       & 0.684     & 0.576 \\ \hline
\end{tabular}
\end{table}

\subsubsection{血腫領域に絞った血腫状態の分類}
本研究では血腫領域のセグメンテーションを行っている。そこで、血腫状態の分類タスクにおいてWavelet CNNの入力の際に、元のCT画像の血腫領域のみを与えることで、血腫状態の分類精度が向上するかを評価した。具体的に、Wavelet CNNの学習の際は、元のCT画像に血腫領域の正解マスクをかけて得られた血腫領域のみの画像を使用する。テスト時は、元のCT画像に、セグメンテーションモデルの出力マスクをかけて得られた画像を使用する。データセットは4つの施設から得られたCT画像を用いた。結果として、マスクをかけて血腫領域を絞ることで、irregularの分類精度は下がったが、hypodensityの分類精度は向上した(表x)。

\begin{table}[h]
\begin{tabular}{|l|l|l|l|}
\hline
条件                                                                & hypodensity & irregular & blend \\ \hline
重み付きwavelet vgg16                                                 & 0.655       & 0.790     & 0.559 \\ \hline
\begin{tabular}[c]{@{}l@{}}重み付きwavelet vgg16\\ + マスク\end{tabular} & 0.676       & 0.732     & 0.559 \\ \hline
\end{tabular}
\end{table}

\subsubsection{Grad Camの一例}
Wavelet CNNモデルより計算されるGrad Camを示す。Grad Camでは、モデルが見ているであろう箇所が強調される。

\begin{figure}[h]
\begin{center}
\includegraphics[width=80mm]{gradcam_wvgg16_weighted_1-4.png}
\caption{
重み付きwavelet vgg16
}
\end{center}
\end{figure}

\begin{figure}[h]
\begin{center}
\includegraphics[width=80mm]{gradcam_wvgg16_weighted_masked.png}
\caption{
重み付きwavelet vgg16 + マスク
}
\end{center}
\end{figure}

\section{おわりに}
脳血腫は6-24時間に急成長を遂げ, 予測を誤り脳外科医が手術しなければ命を
落とす. しかし, 脳血腫には急成長をする型と急成長に至らない型の2通りが
存在し, CTなどによる検査を用いて急成長にいたる脳血腫か否かを人工知能で
分析する技術の開発を行う. この脳血腫の分類問題においては, 正例の少ない
分類問題であること, 血腫の形状が不定であること、その他, 不均衡分類問題,
共変量シフト, 少量データ問題, 疑似相関問題などさまざまなものが存在する.
このため, 単純なVGGなどのCNNを用いた分類においては精度を出すことが難し
い. そこで, 本論文においては, 血腫のセマンティックセグメンテーションと
分類とのジョイント学習を行う方法を提案して, 性能を評価した.