+++ /dev/null
-dnl -*- html -*-
-define(__title, `Master of Mathematics')dnl
-define(__slug, `mmath')dnl
-include(header.html)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/">Prof. 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="__p/bandali-bib.html#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>
-
-<details>
-<summary>Abstract</summary>
-<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>
-</details>
-
-<details open>
-<summary>License</summary>
-<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 <<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>>.
-</pre>
-</details>
-
-<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
projects / ~bandali / bndl.org / blobdiff