% related-work.tex --- other language comparisons -*-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{Related Work}
\label{chp:rw}

In this chapter, we discuss related work on comparing declarative
modelling languages.

The Software~Abstractions book~\cite{Jackson:2012:SAL:2141100}
includes an appendix that discusses alternative modelling languages to
Alloy.  Jackson compares Alloy to four other formal frameworks (B,
OCL, VDM, and Z) by using a simplified version of one of the running
examples used earlier in the book and modelling the example in the
other four languages.  Jackson's comparison consists largely of
discussing the historical background as well as tool support for the
languages, and goes into little detail about the constructs of the
language or a comparison criteria for comparing the languages.

Newcombe~\cite{DBLP:conf/asm/Newcombe14} compares \tla{} and \alloy,
and concludes that \tla's data operations, together with its
higher-order and recursive operators, make descriptions simpler than
\alloy's for engineers, particularly with respect to nested record
structures.  Our comparison looks in detail at the constructs and
semantics of the transition system representations across the
languages, whereas Newcombe focuses on the usage of the languages and
their tool support, as well as more on non-functional criteria such as
each language's minimization of cognitive burden on the modeller, high
return on investment, and the handling of subtle or complex problems.

Zave~\cite{DBLP:journals/fac/Zave15} compares \alloy{} and Spin by
using them to model a complex system, the Chord network protocol for a
distributed hash table, with the goal of recommending a lightweight
formal method for modelling and analyzing complex network protocols.
Zave's comparison includes a few common criteria with ours, such as
implicit vs. explicit snapshot representation, building blocks for
control and data aspects of the model, scope (size bound) of sets, and
the frame problem.  Through modelling and analyzing Chord in \alloy,
Zave arrives at the surprising result that Chord is not correct, as it
was previously thought to be.  Zave notes that although several
previous works had reported on the application of model checking to
implementations of Chord, due to implementations being immensely more
complex than an abstract model, the analyses were necessarily
incomplete.  Although those previous works were able to find bugs in
the implementations they had analyzed, none of them had found the
specification-level bugs that Zave found.  In terms of differences
between \alloy{} and Spin, Zave notes that because the Chord
specification did not include a strong global invariant, she had to
resort to using Spin to find a provably correct global invariant.
Otherwise, Zave notes, the presence of a sufficiently strong global
invariant would have given \alloy{} a performance boost sufficient to
make it the `clear winner' of the comparison (by using the invariant
to restrict the model's reachable snapshot space).

Sullivan \emph{et al.}~\cite{DBLP:conf/sqamia/SullivanWKM17} compare
three snapshot modelling techniques for transition systems in \alloy{}
for performance, using four examples.  They compare two commonly-used
snapshot representation techniques with a new ``parameterization''
approach, in which all signature fields are removed from signature
declarations, and are instead added as arguments to all predicates,
and fact blocks are converted to a predicate, referenced in other
predicates where needed.  Their results suggest that the Alloy
Analyzer exhibits improved performance on examples using their new
parameterization technique.  In contrast to Sullivan \emph{et~al.}'s
work, the focus of our comparison is more generally on the techniques
for modelling transition systems across modelling languages, and we do
not consider the performance of tool support for languages as part of
our comparison criteria.

Frappier \emph{et~al.}~\cite{DBLP:conf/icfem/FrappierFCCO10} compare
six model checking tools (\alloy, CADP, FDR2, NuSMV, ProB, and Spin)
for validation of specification of information systems.  Their
comparison focuses on the ease of specifying behaviours, properties,
and the number of instances that can be checked by each tool for
information systems.  They present the requirements for a library
management system to be modelled and checked with the above tools and
languages.  Their paper is the original source for our library
management case study (Section~\ref{sec:cs/library}).  Frappier
\emph{et~al.}  conclude that a suitable language for validating
information systems using model checking should support a notion of
snapshots and transitions, and that process algebraic operators would
be useful for easily expressing information system scenarios.
Further, they conclude that CTL is powerful enough for expressing the
kinds of properties they are interested in, whereas LTL falls short of
expressing some of the properties.

Deutsch \emph{et~al.}~\cite{DBLP:journals/jcss/DeutschSV07} study the
specification and verification of data-driven information systems,
particularly an interactive web application that receives input from
the user, potentially interacts with a database, and displays output
to the user.  They verify various CTL and CTL$^*$ properties about
their model in an \asm-like specification language based on an earlier
work~\cite{DBLP:phd/dnb/Spielmann00}.

Fraikin \emph{et~al.}~\cite{DBLP:journals/sosym/FraikinFL05} compare
the two specification languages \B{} and \textsc{eb}$^3$,
representative of the snapshot-based and event-based modelling
paradigms respectively, for modelling information systems.  They
compare the two languages by modelling a library information system in
each language, and comparing the models on the four criteria of ease
of specifying functional behaviour, validation, verification, and
evolution of a model to meet new requirements.  The authors conclude
that the two languages are complimentary.  While \B{} seems better at
expressing complex ordering and invariants, \textsc{eb}$^3$ provides a
simpler, modular, explicit representation of temporal properties.  The
downside of \textsc{eb}$^3$'s process algebra is the difficulty of
proving preservation of invariants, since it does not include an
explicit representation of pre and postconditions for transitions,
while \B's drawback is the difficulty of understanding the orderings
of input events, due to the strong data coupling between transitions.

Mazzanti \emph{et~al.}~\cite{DBLP:journals/sttt/MazzantiFS18} study
and report on the use and diversity of formal methods in railway
systems.  They do so in part by modelling and verifying a train
scheduling deadlock avoidance algorithm in seven formal environments
(UMC, Promela/SPIN, NuSMV, mCRL2, FDR4, CPN Tools, and CADP) from
three families of languages (state-machine-oriented, process algebras,
and Petri Nets) and comparing their findings.  The authors observe
that even small decisions in the design and verification process can
result in drastic changes in tooling performance, especially for the
studied process algebraic approaches, but also notice that a model can
be ported to the other environments with limited effort.  The authors
believe this helps propel the new idea of formal methods diversity, in
which modellers port their model to several potentially non-certified
formal tools to increase their confidence in the correctness of the
results of their analysis and verification.  Their paper is the
original source for our railway scheduling deadlock freedom case study
(Section~\ref{sec:cs/railway}).

Aydal \emph{et~al.}~\cite{DBLP:conf/tools/AydalUW08} compare four
tools (USE, Alloy Analyzer, ZLive, and ProZ) for three modelling
languages (UML, \alloy, and Z respectively) with respect to strengths
and weaknesses of the tools for analyzing and verifying the models
written in each language.  In particular, Aydal \emph{et~al.} study
and compare each tool against one another on a course assignment
system example, with four comparison criteria of animation of models,
generation of pre and postconditions for transitions, information
reported about the analysis, and the required expertise.  They also
report on the performance and efficiency of the tools on their models.

Ardis \emph{et~al.}~\cite{DBLP:journals/tse/ArdisCJMPSO96} compare
seven formal languages (Modechart, VFSM, Esterel, Basic LOTOS, Z, SDL,
and C) on the same example, a telephone switching system.  None of the
languages they compare are in the set of languages we compare in this
work.  The criteria that Ardis \emph{et~al.} used to compare the
languages are much higher-level concerns, such as testability and
language maturity, than our comparison, which focuses on how a
transition system model is modelled in a declarative modelling
language.

Huynh \emph{et~al.}~\cite{DBLP:journals/cj/HuynhFPML19} formalize
SCAG, a new healthcare access control model with conflict resolution
for managing each patient's wishes as to who can access their
Electronic Health Records (EHR).  The access control model takes into
account regional laws and regulations applicable in Qu\'ebec and
Canada, where under certain strictly defined scenarios, for safety
reasons, patient consent can be overridden to protect the patient's
life.  The authors formalize the access control policies in \B{} and
\alloy, and use ProB and the Alloy Analyzer to verify properties about
their models.  The results show that without any optimizations, the
Alloy Analyzer performs better than ProB.  However, when using ProB's
capability for controlling the order of constraint solving, as well as
storing frequently-used results in snapshot variables of the \B{}
model, ProB performs significantly better than Alloy for all of the
checked properties.

Bruel \emph{et~al.}~\cite{bruel2019} survey the role of formalism in
system requirements, discussing and comparing more than twenty
approaches to requirements.  They classify the studied approaches into
fives categories of natural language, semi-formal, automata and
graphs, mathematical, and seamless, based on how they express
requirements.  The authors then use a running example of the Landing
Gear System~\cite{DBLP:conf/asm/BoniolW14} to compare the approaches
with respect to nine criteria including level of abstraction, tool
support, separation of the external environment and the system, and
verifiability of requirements.  Bruel \emph{et~al.} present a detailed
and lengthy discussion of their results and conclusions; but in short,
they conclude that formal methods complement other (potentially
informal) requirement approaches, and that they should be seen as
powerful tools available to every requirements engineer or business
analyst.

Leuschel \emph{et~al.}~\cite{DBLP:conf/asm/LeuschelS14} demonstrate
the use of \B{} as a high-level constraint modelling language, with
the ProB tool as the constraint solver.  They compare \B{} and ProB
with \alloy{} and the Alloy Analyzer on several examples, showing the
strengths and weaknesses of each tool on the examples.  The authors
note the ProB solver's weaknesses compared to the Alloy Analyzer on
certain relational operators such as relational image and transitive
closure, citing improvements to these as future work.  Leuschel
\emph{et~al.} conclude that using \B{} with ProB can be a nice
trade-off between the high performance of low-level constraints
solvers and the high difficulty of encoding problems in them, and the
increased computational power needed for solving problems encoded in
higher levels of abstraction.

Samia \emph{et~al.}~\cite{SaWiBeLe09} compare the use of a high-level
specification language and tooling such as \B{} and ProB with a
low-level language and tooling such as Promela and Spin.  They do so
by modelling ten examples in each language and comparing the models on
three criteria of model length, modelling time, and model checking
performance.

Hatcliff \emph{et~al.}~\cite{DBLP:journals/csur/HatcliffLLMP12} survey
designing and using behavioural interface specification languages.
They compare several specification languages \md including JML, SPARK,
Spec\#, and Dafny \md on several examples.  Hatcliff \emph{et~al.}
focus on program verification and languages that allow verifying a
program satisfies certain properties, while our comparison focuses
specifically on modelling transition systems in declarative modelling
languages, at a higher level of abstraction than typical programming
languages.

Maraee and Sturm~\cite{Maraee_2020} examine the usage of the OCL
declarative language with that of the Java imperative programming
language for understanding and developing constraints in a controlled
experiment among a group of undergraduate students.  The obtained
results suggest that using a declarative language such as OCL has many
advantages for understanding and developing constraints over an
imperative language such as Java, with the differences increasing as
the constraints grow more complex.  Writing constraints in a
declarative language enables verification and validation of models,
whereas writing them in an imperative language inevitably shifts the
focus to low-level implementation details that are irrelevant to the
essence of the constraints.

Lamport and Paulson~\cite{DBLP:journals/toplas/LamportP99} compare
specification with and without a type system, stating advantages and
disadvantages for both typed and untyped specification languages.
They compare set theory and typed formalisms across four general
criteria of flexibility, convenience, pitfalls, and abstractness; and
conclude that an untyped set theory could serve as a solid, common
foundation upon which different tool-specific type systems can be
overlaid.

L\'{o}pez \emph{et~al.}~\cite{DBLP:conf/amast/LopezNR06} propose a
formal framework for assessing the expressivity of formal
specification languages, based on the mutation testing technique.  The
idea is to create mutated versions of a specification that differ from
the original specification in some aspect, with some of the mutants
still exhibiting correct behaviour and some behaving incorrectly.
Then, model the mutants in the specification language under study.
The authors' measure of expressivity and suitability of languages for
modelling a certain class of systems is based on the ratio of the
correctness of mutants and the correctness of the models of those
mutants in the given modelling language.  In other words, whether the
models of the correct and incorrect mutants are distinguishable in the
modelling language.

Some textbooks~\cite{Nissanke_1999, DBLP:series/txcs/AlagarP98,
  DBLP:books/daglib/0016252, Bjorner:2007:LSL:1349804,
  Lauesen:2001:SRS:773258, Bjorner:2007:LSL:1349804,
  DBLP:series/txcs/AlagarP11, DBLP:series/utcs/ORegan17a} introduce
various formal and informal modelling languages, each with their own
examples or occasionally the same example, to illustrate certain
aspects of the language.  However, they generally do not compare the
languages against one another.

In comparison to these related works, 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.


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