dnl -*- html -*-
define(__title, `Master of Mathematics')dnl
define(__slug, `mmath')dnl
include(header.html)dnl
define(__latex, `<span class="t-logo">L<sup>a</sup>T<sub>e</sub>X</span>')dnl

<article>
<h1>Master of Mathematics</h1>

<p class="justify">I graduated from the University of Waterloo with
the degree of Master of Mathematics in Computer Science in Spring
2020.  My research at the <a href="//watform.uwaterloo.ca">Waterloo
Formal Methods</a> group focused on formal logic, model checking, and
verification; under supervision of
<a href="//cs.uwaterloo.ca/~nday/">Dr. Nancy Day</a>.</p>

<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
dnl
dnl<p><em>Jump to:</em>
dnl<a href="#thesis">thesis</a> |
dnl<a href="#presentation">presentation</a> |
dnl<a href="#models">models</a></p>

<h3 id="thesis">Thesis</h3>

<p>Reference version:
<a href="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
<a href="bandali-bib#bandali2020">bib</a><br/>
__latex sources:
<a href="//p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
<a href="//p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>

<h4 class="center-text">Abstract</h4>
<blockquote id="abstract">
<p>Declarative behavioural modelling is a powerful modelling paradigm
that enables users to model system functionality abstractly and
formally.  An abstract model is a concise and compact representation
of key characteristics of a system, and enables the stakeholders to
reason about the correctness of the system in the early stages of
development.</p>

<p>There are many different declarative languages and they have
greatly varying constructs for representing a transition system, and
they sometimes differ in rather subtle ways.  In this thesis, we
compare seven formal declarative modelling languages B, Event-B,
Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
criteria.  We classify these criteria under three main categories:
structuring transition systems (control modelling), data descriptions
in transition systems (data modelling), and modularity aspects of
modelling.  We developed this comparison by completing a set of case
studies across the data- vs. control-oriented spectrum in all of the
above languages.</p>

<p>Structurally, a transition system is comprised of a snapshot
declaration and snapshot space, initialization, and a transition
relation, which is potentially composed of individual transitions.  We
meticulously outline the differences between the languages with
respect to how the modeller would express each of the above components
of a transition system in each language, and include discussions
regarding stuttering and inconsistencies in the transition relation.
Data-related aspects of a formal model include use of basic and
composite datatypes, well-formedness and typechecking, and separation
of name spaces with respect to global and local variables.  Modularity
criteria includes subtransition systems and data decomposition.  We
employ a series of small and concise exemplars we have devised to
highlight these differences in each language.  To help modellers
answer the important question of which declarative modelling language
may be most suited for modelling their system, we present
recommendations based on our observations about the differentiating
characteristics of each of these languages.</p>
</blockquote>

<h4>License</h4>

<pre>
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 &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
</pre>

<p>A copy of the GNU General Public License is available
from <a href="gpl-3.0.html">gpl-3.0.html</a>, as well as in
the <code>COPYING</code> file included in both of the __latex source
archives linked above.</p>

<h3 id="presentation">Presentation</h3>

<p>Reference version:
pdf (coming soon)<br/>
__latex sources:
tar.gz | zip (coming soon)</p>

<p>This is the presentation I delivered to my supervisor and the
second readers of my thesis on Jun 30, 2020, as
<a href="//cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
on the Cheriton School of Computer Science website.</p>

<h3 id="models">Models</h3>

<p>Reference version:
tar.gz | zip (coming soon)</p>
</article>

define(__copy, `2020')dnl
include(footer.html)dnl