% introduction.tex --- thesis introduction -*-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{Introduction}
\label{chp:intro}

\vspace{-1.5em}
\setlength\epigraphwidth{.42\textwidth}
\setlength\epigraphrule{0pt}
\epigraph{\itshape Architects draw detailed plans before a brick is
  laid or a nail is hammered.  Programmers and software engineers
  do not.  Can this be why houses seldom collapse and programs often
  crash?}{\footnotesize --- Leslie Lamport, Turing Award Winner, 2013}
\vspace{0.5em}

\noindent
Distinguished Computer Scientist Leslie Lamport explains that
blueprints help architects make sure what they are planning to build
will work.  Furthermore, ``working'' means more than merely not
collapsing, but rather serving the intended purpose.  Engineers and
architects use blueprints as a common language between themselves and
their clients, and use it to precisely plan out ahead of time the
structure that they will build.  However, programmers and software
engineers rarely even sketch out what their programs are intended to
do, before starting to write the code.  Even the simplest and most
commonly taught algorithms such as binary sort sometimes require
careful thinking about their intricate details to ensure their
correctness, let alone complex systems with dozens or more subsystems
and parts intended to work together.

When designing complex systems, Lamport argues, the need for formal
specifications should be as obvious as the need for blueprints when
designing a skyscraper.  However, few programmers even know of
existence of specification languages and their supporting tools, much
less how to use and write specifications for the systems they design.

There are a number of reasons why formal specifications are important
and useful.  Most mainstream programming languages currently commonly
used by programmers, such as C, C++, or Java, usually require
programmers to be deep into the implementation details, imperatively
specifying exactly how each task should be carried out.  It is often
challenging to keep in mind the big picture of what the parts are
supposed to do individually and as a group, without getting bogged
down with other less relevant details.  Having formal specifications
in one's toolbox enables abstracting away from irrelevant details,
focusing only on the heart of the matter and making sure it is well
understood, and that the proposed solution correctly fits and serves
the required purpose.


\section{Declarative Modelling Languages}
\label{sec:intro/dml}

The languages studied in this thesis are declarative modelling
languages for behavioural formal specification using a
state-machine-oriented/transition system approach.  These languages in
essence model a Kripke structure underneath.  Declarative behavioural
modelling is a powerful technique for modelling systems in a concise
way, free of design or implementation details.  Declarative modelling
languages allow describing systems in a higher level of abstraction
than permitted by typical mainstream programming languages like C or
Java.

Models written using declarative behavioural modelling languages, such
as Z~\cite{DBLP:books/daglib/0068766},
\alloy~\cite{Jackson:2012:SAL:2141100}, and
\tla{}~\cite{DBLP:books/aw/Lamport2002}, have the following general
characteristics~\cite{DBLP:conf/re/AbbassiBDS18}:
\begin{enumerate}
  \item they describe the transitions in a declarative manner using
    constraints, rather than through imperative calculations and/or
    statements;
  \item they include user-defined and -axiomatized units of data,
    which can represent rich datatypes such as lists and trees;
  \item they have a formal mathematical and logical foundation,
    usually first-order logic (FOL) and/or set theory; and
  \item they allow writing models without specifying the size of sets
    (the scopes); the scopes may need to be specified for analysis.
\end{enumerate}

We are motivated to do this study by the many applications and
demonstrated usefulness of declarative modelling languages and model
checking to help design systems or analyze and verify properties about
the design of existing systems.  Examples include Zave's use of
\alloy{} and Spin to find specification-level bugs in the
specification of the Chord network
protocol~\cite{DBLP:journals/fac/Zave15}, Newcombe's report on the use
of \tla{} by engineers at Amazon which has helped find subtle bugs in
complex real-world systems and prevent the bugs from reaching
production~\cite{DBLP:conf/asm/Newcombe14}, and the use of \B{} by
Huynh \emph{et~al.} for formalizing a new healthcare access control
model with conflict resolution for managing patients' consent as to
who can access their Electronic Health Records (EHR), while taking
into account the regional laws and regulations of Qu\'ebec and Canada
that allow overriding patient consent regarding access to their EHR
under certain strictly defined scenarios to protect the patient's
life~\cite{DBLP:journals/cj/HuynhFPML19}.

Declarative models allow modellers to sketch out and reason about
systems and how they change over time in an abstract and declarative
way, without having to worry about irrelevant details.  An important
question, given that there are a great many number of languages to
choose from, is how does one make a choice of which language to use?
This thesis presents a comparison criteria and compares a number of
popular declarative languages, highlighting the control and data
modelling aspects, as well as the modularity of models in each
language.  Comparisons between modelling languages are useful to
provide a means of discerning which modelling language is most
suitable for modelling a system.  Models in these languages may vary
in length and organization, and doing a number of case studies in
multiple languages helps us better expose the differences in
paradigms, conventions, and structures among the languages.  Common
constructs in the languages often vary in subtle ways, and through our
case studies, we tease these differences apart for each language.  The
equivalence of our models is by observation, using a model checker and
potentially other available tool support for each language to verify a
series of properties about the models across all of the selected
languages.

In comparison to other works comparing declarative modelling
languages~\cite{DBLP:conf/asm/Newcombe14, DBLP:journals/fac/Zave15,
  DBLP:conf/icfem/FrappierFCCO10, DBLP:journals/tse/ArdisCJMPSO96}, we
focus on models of transition systems.  We develop a set of
categorized comparison criteria and examine in depth each language
with respect to each of the criterion.  Further, we use these criteria
to compare a diverse range of examples on the data-
vs. control-oriented characterization spectrum, modelling each of the
five examples in all of the seven languages, producing a total of
thirty-five models.  We use these models and our observations from
carrying out the case studies to make recommendations as to which
language(s) we think would be the best fit for modelling various kinds
of transition systems.


\section{Selection of Languages}
\label{sec:intro/sel}

We selected the seven popular, declarative modelling languages
\B~\cite{DBLP:books/daglib/0015096},
\eventb~\cite{DBLP:books/daglib/0024570},
\alloy~\cite{Jackson:2012:SAL:2141100}, \dash~\cite{serna2019},
\tla~\cite{DBLP:books/aw/Lamport2002},
\pluscal~\cite{DBLP:conf/ictac/Lamport09}, and
\asmetal~\cite{DBLP:journals/jucs/GargantiniRS08} for comparison.  We
chose languages that have tool support for model checking.  However,
we are not comparing the languages on their tool support, because tool
support and the analysis performance of those tools are subject to
change, and can change much more easily than the logic and semantics
of the language.  This point of view is also shared by Lamport, with
\tla{} existing for several years before the \tlc{} model checker and
the rest of the \tla{} Toolbox were created for it.

We did not include other formal specification languages for various
reasons.  For instance, we omitted the
Z~\cite{DBLP:books/daglib/0068766} and
VDM~\cite{DBLP:books/daglib/0067105} specification languages, due to
the lack of model checking tool support for them, and formalisms based
on process algebras and Petri Nets, as they are at a different (often
lower) level of abstraction compared to declarative modelling
languages.  We also did not include
Electrum~\cite{DBLP:conf/sigsoft/MacedoBCCK16,
  DBLP:conf/kbse/BrunelCCM18, DBLP:journals/sttt/CunhaM20}, another
extension of \alloy, as we decided to include at most one extension
for each language, and we found \dash{} and its features to be a
bigger change from \alloy{} than Electrum.

Statecharts-based languages and UML state machines~\cite{uml} provide
a graphical manner to describe system behaviour, but do not completely
fall into the category of declarative specification languages: their
semantics are often not fully formal and they lack support for
declaring datatypes.  OCL~\cite{ocl} is a declarative language that
can be used in combination with UML to constrain the pre and
postconditions of transitions.

The languages of model checkers such as SMV~\cite{McMillan_1993} and
Spin~\cite{DBLP:books/daglib/0020982} are lower-level descriptions
than what is often convenient for a user.
nuXmv~\cite{DBLP:conf/cav/CavadaCDGMMMRT14} is a re-implementation and
extension of SMV that adds support for verification of infinite
datatypes, such as integers and reals, and incorporates a verification
engine with state-of-the-art \sat-based algorithms.  However, they all
have limited support for user-declared datatypes.  Furthermore, in
SMV/nuXmv the scope of datatypes and relations must be set at
modelling time, which forces users to modify their models every time
they want to analyze and check properties in at larger scope.


\section{Thesis Contributions}
\label{sec:thesis-contributions}

The contributions of this thesis are
\begin{itemize}
\item a set of criteria to compare declarative modelling languages;
\item a diverse set of case studies on the data- vs. control-oriented
  characterization spectrum;
\item the comparison of the selected declarative modelling languages
  (\B, \eventb, \alloy, \dash, \tla, \pluscal, and \asmetal) based on
  these criteria by carrying out the case studies; and
\item our recommendations for the choice of modelling language based
  on the characteristics of the transition system under description,
  rooted in our observations of the differences and similarities
  between the languages with respect to our comparison criteria from
  the several case studies we carried out.
\end{itemize}

The overview of the methodology for comparing the selected languages
for this thesis is to do a number of case studies in each language,
taking notes on their characteristics and differences while doing so.
Each of the chosen case studies is a model previously done in one (or
possibly more) of the selected languages.  The choice of the order of
languages for each case study was made randomly to address any
potential concerns for bias in that regard.


\section{Thesis Outline}
\label{sec:intro/outline}

Chapter~\ref{chp:bg} provides background on the seven declarative
modelling languages used in this work.  Chapter~\ref{chp:methodology}
describes our methodology for carrying out the research and modelling
of the case studies across the languages, as well as addressing
potential threats to validity.  In Chapter~\ref{chp:control}, we
discuss the control modelling aspects in each language, meaning the
structuring of transition systems in terms of a individual
transitions, in Chapter~\ref{chp:data} we consider the data modelling
aspects of each language and the structuring of transition systems in
terms of their data descriptions, and in Chapter~\ref{chp:mod} we
investigate the constructs relating to modularity of models in the
languages and the structuring of transition systems on a larger scale
in terms of files as well as subtransition systems.
Chapter~\ref{chp:cs} provides an overview of our case studies, and how
our comparison criteria highlighted interesting and/or different
features and characteristics of each language while modelling each
case study.  Chapter~\ref{chp:recs} presents recommendations for the
choice of declarative modelling language based on the characteristics
of the transition system under description.  Finally,
Chapter~\ref{chp:rw} presents related work, and
Chapter~\ref{chp:conclusion} provides concluding remarks.


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