% background.tex --- background on the selected languages -*-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{Background}
\label{chp:bg}

In this chapter, we provide background on the seven declarative
modelling languages we selected to study and carry out our case
studies in this work.  For each language, we give a brief background
about its history and origins, and its logic.  Detailed information
about the language will be covered in the comparisons of the following
chapters.  We also report on the tools we used to support our
modelling efforts.  Information about the version of each tool we used
is available in Appendix~\ref{appx:vers}.

As we will be frequently referring to languages by name in the next
chapters of this thesis, to make the language names easier to spot and
discussions easier to follow, we adopt the language name stylizations
shown in Table~\ref{tab:bg/langs}.  Further, the keywords in each of
the languages are colour-coded, to help make distinguishing between
the code snippets across the languages easier in later chapters.

\begin{table}[h]
  \centering
  \caption{Language name stylizations and colours}
  \label{tab:bg/langs}
  \input{table/bg-langs}
\end{table}


\section{B}
\label{sec:bg/b}

\B~\cite{DBLP:books/daglib/0015096,b-manref} is a formal method
originally developed by Jean-Raymond Abrial in the 1980s as a
successor to Z, and using an Abstract Machine Notation (\amn) for
specification of systems.  \B{} is used in the development of correct
by construction software, with tool support for specification, design,
and verification (animating, model checking, and theorem proving) of
software systems.

The logic of \B{} is rooted in first-order logic and set theory.  Sets
are created using either set comprehension, or set operations (such as
Cartesian product, intersection, power set, \emph{etc.}) and can be
used for updating a variable's value to create a transition system.
Predicates can be axiomatized or defined using propositional logic
operations and set predicates.  Functions can be declared both
explicitly using function types (partial, total, surjective,
\emph{etc.}), or implicitly by restricting relations.  \B{} supports
\emph{refinement} of machines, allowing the modeller to start at a
high level of abstraction, and gradually refine their model to more
concrete ones.

Given \B's longevity, various tooling software has been developed over
the years to support the \B{} method and development of \B{} models.
These include the B-Toolkit originally developed by B-Core and now
available as free software~\cite{freesw} under the 2-clause BSD
license~\cite{b-toolkit-license}, the proprietary Atelier B industrial
tool developed by ClearSy, and the ProB animator and model
checker~\cite{DBLP:conf/fm/LeuschelB03} released as free software
under the EPL v1.0 license~\cite{prob-license}.  We used the ProB tool
for writing and checking our \B{} models.


\section{Event-B}
\label{sec:bg/eventb}

\eventb~\cite{DBLP:books/daglib/0024570} is a simplification and
extension of the \B{} method.  While \B{} is largely used for
specification and verification of software systems, \eventb{} was
designed to enable the modelling of complete systems (software,
hardware, as well as the surrounding environment), merging the gap
between specification of the software and the rest of the system.
\eventb{} is a successor of \B, and its logic is very similar to that
of \B{} and is rooted in first-order logic and set theory.

Although \eventb{} is a successor of \B{} and its syntax is a
simplification and extension of that of \B, where a \B{} model is
simply a plaintext file with its content directly matching the \B{}
syntax, an \eventb{} model is a series of multiple complex XML files.
This means \B{} models can easily be read and written using any text
editor, but reading and writing \eventb{} models effectively requires
a special-purpose text editor for parsing and modifying the XML files
without getting in the way of the modeller.  At the time of writing
this work, the only available tool support for \eventb{} is the Rodin
Platform~\cite{DBLP:journals/sttt/AbrialBHHMV10,rodin-handbook}, an
eclipse-based IDE released as free software under the EPL v1.0
license~\cite{rodin-license}.  The Rodin Platform comprises a set of
plugins, including a text editor for creating and editing \eventb{}
models, plugins for integration with the ProB animator and model
checker, a \LaTeX{} exporter plugin for generating typeset documents
from \eventb{} models, and more.  Even though the Rodin Platform's
model editor is capable of editing \eventb{} models, the user has to
point and click or use several keyboard shortcuts to make various
parts of the model description editable.  We believe that this, along
with the fact that the text editor is barely customizable, makes Rodin
less suitable for writing larger models.

Lastly, the current latest release of the Rodin Platform as of the
time of this writing is over two years old, and is based on a version
of Eclipse that suffers from a known bug that causes it to crash
immediately when used with any Java version newer than Java 8.
Considering that many GNU/Linux distributions have been dropping this
old release of Java from their repositories, and as time goes by more
distributions continue to do so, this effectively means that the Rodin
Platform cannot be used on newer machines and operating systems.

For the \eventb{} models of our case studies, we used the Rodin
Platform, as well as the ProB plugin for Rodin, which supports
exporting \eventb{} models from the Rodin Platform for analysis using
the standalone ProB tool.


\section{Alloy}
\label{sec:bg/alloy}

\alloy~\cite{DBLP:journals/tosem/Jackson02,Jackson:2012:SAL:2141100}
is a declarative modelling language designed for exploring and
describing structures and their properties.  \alloy's logic is a
relational logic with set theory, that is both powerful enough to
express complex structures and constraints on them while allowing
fully automated analysis of models written in the language.

\alloy{} is primarily supported by the Alloy
Analyzer~\cite{Jackson:2012:SAL:2141100} tool, a finite model finder
for analyzing \alloy{} models by finding satisfying instances for
predicates or counterexamples to assertions in finite scopes.  The
Alloy Analyzer comes with a visualizer and evaluator, which are
invaluable for visualizing generated instances and evaluating \alloy{}
expressions when writing or debugging \alloy{} models.  Properties to
be checked are written in \alloy{} itself as predicates or assertions
along with the main specification of the model.  The Alloy Analyzer
through Kodkod~\cite{DBLP:conf/tacas/TorlakJ07} integrates with
multiple \sat{} solvers, allowing the modeller to easily switch
solvers and choose the one that performs the best for their use-case.

Besides the Alloy Analyzer, a variety of other tools have been
developed by the Alloy community.  These include
Astra~\cite{abbassi2018} for Alloy to SMT-LIB translation, as an
alternative to Kodkod; and ALDB~\cite{aldb-src}, a command-line tool
for debugging transition system models written in \alloy{}, which
allows the modeller to step through the transitions of a transition
system model, similar to stepping through the lines of code of a
program using a debugger for a programming language.

In \alloy, there are multiple possible approaches for constructing
snapshot traces for model checking; for instance by using \alloy's
built-in \alloycode{util/ordering} module for imposing a linear total
order on snapshots, or using transitive closure-based approaches,
\emph{e.g.} as used in the CTL modules developed for \alloy{} for
transitive closure-based model checking
(TCMC)~\cite{DBLP:journals/sosym/FarheenDVA20}.  For our case studies,
we used both of these methods for model checking our \alloy{} models.
In this work, we will not consider the construction of traces to be a
part of the model.


\section{Dash}
\label{sec:bg/dash}

\dash~\cite{DBLP:conf/re/SernaDF17,serna2019} is a new modelling
language for writing declarative behavioural models, combining the
logic of \alloy{} with common control-oriented modelling constructs of
labelled control state hierarchy and named events, as introduced by
Harel~\cite{DBLP:journals/scp/Harel87}.  \dash{} is built as an
extension to \alloy, with its language being a superset of the
\alloy{} language.  \dash{} provides syntactic constructs for
specifying and factoring transitions.  Transitions can be factored by
states, like in Statecharts, or by events and/or conditions; making
\dash{} a flexible language capable of accommodating different
modelling paradigms.  \dash{} implements transition comprehensions,
enabling the description of a group of transitions using a single
statement.  \dash{} follows the usual semantics of Statecharts:
transitions from states higher in the hierarchy have priority over
those lower in the hierarchy, and concurrent states can each take one
transition in response to an environmental input forming big steps
(consisting of multiple transitions).  Properties to be checked are
written along with the main specification of the model either in the
form of \alloy{} expressions in \dashcode{escape} blocks, or in a
small domain-specific subset of \dash, based on the underlying CTL
module (TCMC) used by \dash's tool support for model checking.

Tooling around \dash{} is built using Xtext~\cite{xtext}, and includes
a compiler for translating \dash{} to \alloy, allowing the modeller to
benefit from use of the Alloy Analyzer for model
checking~\cite{SeDa18} and model finding like regular \alloy{} models.
A text editor with syntax highlighting for \dash{} is available as an
Eclipse plugin.  Also, the \dash{} website at
<\url{http://dash.uwaterloo.ca:8080/dash/}> includes an online editor
for writing \dash{} models and translating them to \alloy{} in the
browser.


\section{TLA${}^+$}
\label{sec:bg/tla}

\tla~\cite{DBLP:books/aw/Lamport2002} is a formal specification
language developed by Leslie Lamport, based on the idea that using
simple mathematics is the best way to write formal descriptions; and
that a specification language should provide the bare minimum required
for writing simple mathematics to describe systems precisely.  \tla{}
has first-order logic with an untyped classical set theory as its
modelling language, and was originally designed for writing high-level
specifications of reactive, distributed, and asynchronous systems.
LTL properties to be checked are written along with the main
specification of the model using the full \tla{} language, including
several temporal operators such as $\Diamond$ and $\Box$ for expressing temporal
properties.

Tool support for \tla{} is mainly the \tla{} Toolbox, an Eclipse-based
IDE tailored for writing and working with \tla{} specifications.  The
\tla{} Toolbox includes the SANY parser and semantic analyzer for
\tla, the TLC model
checker~\cite{DBLP:conf/charme/YuML99,DBLP:books/aw/Lamport2002}, the
\pluscal{} algorithm language~\cite{DBLP:conf/ictac/Lamport09}, the
TLA\TeX{} pretty printer~\cite{DBLP:books/aw/Lamport2002}, and the
TLAPS (\tla{} Proof System)~\cite{DBLP:conf/cade/ChaudhuriDLM10}.
\tla{} supports model refinement.

For the \tla{} models of our case studies in this work, we used the
\tla{} Toolbox and the \tlc{} model checker, which is already set to
use multiple worker threads out of the box.  For model checking very
large models, \tlc{} can run on a cluster of compute nodes.


\section{PlusCal}
\label{sec:bg/pluscal}

\pluscal~\cite{DBLP:conf/ictac/Lamport09} is a formal specification
language created by Leslie Lamport fifteen years after \tla{} for
describing and reasoning about algorithms, as an alternative to
traditional informal pseudocode.  \pluscal{} has two separate
syntaxes: a C-syntax~\cite{pluscal-c-syntax} similar to the C family
of programming languages, and a more verbose but clearer
P-syntax~\cite{pluscal-p-syntax} which we have opted to use in this
work.  The verbosity of the P-syntax makes the meaning of the code
clearer.  While each of \pluscal's syntaxes resemble that of an
imperative programming language, semantically \pluscal{} is more
expressive than a programming language, since any mathematical formula
that can be represented in \tla{} may be used as a \pluscal{}
expression.  \pluscal{} models are translated into \tla, and may then
be verified using the \tlc{} model checker and the other \tla{} tools.
LTL properties to be checked are written using the full \tla{}
language, including several temporal operators such as $\Diamond$ and $\Box$ for
expressing temporal properties.

For our \pluscal{} models, we used the \tla{} Toolbox, which as
described above, has a plugin for translating \pluscal{} to \tla.  The
\pluscal{} syntax is embedded in \tla{} as a special block comment in
a \tla{} module.


\section{AsmetaL}
\label{sec:bg/asmetal}

\asmetal~\cite{DBLP:conf/asm/ScandurraGGGR05,
  conf/3m4mda/GargantiniRS06, DBLP:journals/jucs/GargantiniRS08}
(Asmeta Language) is a modelling language developed by Gargantini
\emph{et~al.} as part of the Asmeta framework, based on the Abstract
State Machines (\asm{}s)~\cite{DBLP:books/sp/BorgerS2003,gurevich1984}
formal method.  The logic of \asmetal{} is first-order logic, with
added semantics for snapshot variable updates and transition
definitions, as formalized in~\cite{DBLP:books/sp/BorgerS2003}.
Properties to be checked are written along with the main specification
of the model using \asmetal{} expressions, as well as additional LTL
and CTL temporal operators available from libraries distributed with
the model checker.  Asmeta is a framework comprised of a variety of
tools to aid with validation and verification of \asm{} models.  At
the time of writing this work, Asmeta is an active research project
consisting of an extensive collection of tools for verification and
validation of \asm{}s, released as free software~\cite{freesw} under
the GPLv2+ license~\cite{asmeta-license,gplv2}.

The most relevant of these tools for our comparison are the
\textbf{Asmee} editor for \asmetal, the \textbf{AsmetaLc} compiler and
parser for \asmetal, the \textbf{AsmetaS} simulator, the
\textbf{AsmetaA} animator, and the \textbf{AsmetaSMV} model checker
based on NuSMV.  As our work is centred around a comparison of
modelling languages with model checking tool support, we were hoping
to make extensive use of the various Asmeta tools, especially the
AsmetaSMV model checker, which supports model checking both LTL and
CTL properties.  Unfortunately, we found that AsmetaSMV currently only
supports a limited subset of the \asmetal{} language, and we ran into
these limitations with our models.  Further, we learned that the
AsmetaA animator and AsmetaS simulator suffer from similar
limitations.  For our case studies, since our goal is to compare the
modelling languages and not their available tool support, we opted to
use the full capabilities of the \asmetal{} language, which is not yet
fully supported by the tooling as of today.  As such, for verifying
our \asmetal{} models we rely on the parser and typechecker for
\asmetal, and additionally the animator and simulator when possible.


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