% methodology.tex --- thesis methodology -*-latex-*-

% Copyright (C) 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


\chapter{Methodology}
\label{chp:methodology}

In this chapter we describe the methodology used for carrying out the
research and modelling of the case studies across the languages.  We
describe the principles put into designing our methodology, including
how we devised the comparison criteria, and the measures we took to
avoid bias in the work as much as possible.

To compare declarative modelling languages for writing models of
transition systems, we began by selecting six relatively small
examples and modelled them in three declarative modelling languages,
with help from my colleagues and now former students Ali Abbassi and
Jose Serna.  We collaborated while writing the models, answering each
other's questions and providing clarifications about any aspect of the
models.  These examples are those \emph{without} an asterisk in
Figure~\ref{fig:methodology/cs} of the data- vs. control-oriented
characterization spectrum.  A model is more control-oriented if it has
complex conditions for when a transition is relevant that are
naturally expressed using modes, control states, or concurrency.  A
model is more data-oriented if it has complex constructions of data.
Based on our experience modelling these examples, we described the
differences and similarities we observed across the languages, forming
an initial set of comparison criteria to compare the languages
against; and published our results~\cite{DBLP:conf/re/AbbassiBDS18}.
These criteria included datatypes and typechecking, expressions,
constructs for specifying the structure of transition systems and
their semantics, and scalability of models.

\input{figure/methodology-cs}

Next, we expanded on our initial set of comparison criteria to include
other interesting characteristics of declarative modelling languages
that we did not previously consider, such as the various kinds of
inconsistency in models, the detailed discussions about
well-formedness, and decomposition of a transition system into
subtransition systems.  Further, we expanded our set of chosen
declarative modelling languages from the initial three languages (\B,
\dash, and \tla) to include \asmetal, \alloy, \eventb, and \pluscal{}
as well.  We then chose a diverse set of examples from across the
characterization spectrum from our initial set of examples.  These
were the three most interesting and non-trivial examples among the
ones we already had.  We modelled these examples in the newly added
languages as well, helping us make sure we correctly set up the tool
support available for all of the languages.

Having made sure we are set up to use the supporting tools available
for each language by modelling our previous examples in the newly
added languages, we expanded our set of examples with two new larger
systems.  These two are the Library and Railway systems, marked with
an asterisk in Figure~\ref{fig:methodology/cs}.  Collectively, we
increased our number of models from eighteen (six models in three
languages) small models to thirty-five (five models in seven
languages) including larger examples.  Our final case studies are
those typeset in \textbf{bold} in Figure~\ref{fig:methodology/cs},
presented in this thesis.  Table~\ref{tab:cs/loc} in
Chapter~\ref{chp:cs} shows the sizes of the models in the common
measuring unit Lines of Code, highlighting our use of larger and
realistic examples for our case studies in this work.

Table~\ref{tab:methodology/cs-orders} shows the case studies and
languages considered in this work.  For each case study (row), the
number in each column indicates the order in which the model was
completed in that language.  We tried to make the table such that most
columns include either a 1 or an E, meaning that at least one of the
case studies was first modelled by us in that language, or originated
in that language.  We then used that version as the reference model
for the next models of that case study ported to the other languages.
Our first three models of EHealth, digital watch, and musical chairs
were completed concurrently, and thus are all labelled `1' in the
table.  For the case studies where no reference model was available,
we used the informal or semi-formal description of the system from the
originating paper to write a first model, and used that model as our
reference for the subsequent models of the case study.  To avoid any
bias, we assigned a random order to each model of each case study in
each of the languages.  We carried out the case studies top to bottom,
starting with the EHealth system and ending with Railway, learning new
languages as needed.  While doing so, we observed and took notes about
various characteristics of the modelling languages according to our
comparison criteria, focusing on those used in the current model, and
how we believed they affected the modelling process.  With the help of
these notes, we later developed isolated exemplars, which are small
examples meant to demonstrate the differences between languages with
respect to a particular criterion.  If a model needed updating
(\emph{e.g.} addition of new properties, new criteria, new insights,
\emph{etc.}), we iterated through the versions of the model in all
languages, updating those accordingly as well.  Through this process
we further expanded our set of comparison criteria.

\begin{table}[h]
  \centering
  \caption{Order of modelling case studies across languages}
  \label{tab:methodology/cs-orders}
  \input{table/methodology-cs-orders}
  \begin{minipage}{0.9\textwidth}
    \vspace{0.5em} \textit{Legend:} E indicates \underline{E}xisting
    models, \emph{i.e.} those that we had no influence on.  The
    numbers in each row indicate the order of languages the case study
    was done in.
  \end{minipage}
\end{table}

Our methodology was designed to limit bias towards one language or
another when drawing our conclusions regarding language comparisons
and recommendations based on them.  For threats to validity, a
possible threat to \emph{internal validity} is that not all languages
were the source/reference language in which a case study was modelled
in.  To partially alleviate this, we made sure that at least most of
the chosen languages were the source/reference for at least one case
study.  To further minimize threats to internal validity, we
randomized the order in which we carried out each case study across
the languages.  A possible threat to \emph{external validity} is that
we may be missing comparison criteria that could have risen have we
had done more case studies.  Further, we only have five examples as
part of our case studies.  To partially remedy this, we made sure to
use a diverse set of examples across the data- vs. control-oriented
characterization spectrum, and of different sizes.  A possible threat
to \emph{construct validity} is that our recommendations for each case
study may be biased by our previous knowledge of some language, as we
are more familiar with some languages more than others.  To alleviate
this bias, we have included multiple new languages and new case
studies, that we were not previously familiar with.  Another potential
threat to construct validity is not all of our models may follow all
the idioms of the languages, due to the modeller being a novice user
of some the languages.  To partially remedy this, we use \underline{E}
models as references for our models of case studies whenever they are
available to us.  Further, our comparison criteria are very
syntax-based, thus our comparison is not based on idioms and writing
idiomatic models.  Threats to \emph{conclusion validity} are those
concerning the validity of our conclusions and recommendations about
the choice of modelling language.  To address these, we devised an
extensive set of comparison criteria to compare the languages against
while carrying out the case studies, and used a diverse set of
examples for our case studies based on which we make our
recommendations.


%% Local Variables:
%% tex-main-file: "../bandali-mmath-thesis.tex"
%% End:
