X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/bfc8d4d89f34cdb2609bbab4f0b60c5ca395d5a8..a0e46d57508b45f23f360daa9ba6432e2b2f19f5:/mmath.html
diff --git a/mmath.html b/mmath.html
new file mode 100644
index 0000000..91d9097
--- /dev/null
+++ b/mmath.html
@@ -0,0 +1,172 @@
+<!doctype html>
+<html lang="en">
+<head>
+<meta charset="utf-8" />
+<meta name="author" content="bandali" />
+<meta name="viewport" content="width=device-width, initial-scale=1" />
+<title>master of mathematics — bandali</title>
+<link rel="canonical" href="https://bndl.org/mmath.html" />
+<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
+<style>
+body {
+ line-height: 1.6;
+ max-width: 37.5em;
+ margin: 0 auto;
+ padding: 0 1em;
+}
+details { margin: 1em 0; }
+details summary { cursor: pointer; }
+#copy { font-size: 0.84em; }
+#copy p { padding: 0 2em; }
+blockquote { text-align: justify; }
+.tex {
+ font-family: "Tex Gyre Termes", serif;
+ text-transform: uppercase;
+}
+.tex sub {
+ font-size: 1em;
+ margin-left: -0.1667em;
+ margin-right: -0.125em;
+ vertical-align: -0.5ex;
+}
+.tex sup {
+ font-size: 0.85em;
+ margin-left: -0.36em;
+ margin-right: -0.15em;
+ vertical-align: 0.15em;
+}
+.box {
+ background: #f8f8f8;
+ border: 1px solid #e6e6e6;
+ border-radius: 4px;
+ font-size: 0.95em;
+ padding: 0.6em 0.9em;
+}
+@media (prefers-color-scheme: dark) {
+ body { background: #1c1c1c; color: white; }
+ a:link { color: #acdeff; }
+ a:visited { color: #f8f; }
+ a:active { color: #e00; }
+ .box { background: #1b1d1e; border-color: #373c34; }
+}
+</style>
+</head>
+<body>
+<h1><a href=".">bandali</a>'s master of mathematics</h1>
+
+<p>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="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
+group focused on formal logic, model checking, and verification; under
+supervision of
+<a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy Day</a>.</p>
+
+<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
+
+<!-- <p><em>Jump to:</em>
+<a href="#thesis">thesis</a> |
+<a href="#presentation">presentation</a> |
+<a href="#models">models</a></p> -->
+
+<h3 id="thesis">Thesis</h3>
+
+<p>Reference version:
+<a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
+<a href="bandali-bib.html#bandali2020">bib</a><br />
+
+<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
+<a href="https://p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
+<a href="https://p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
+
+<details class="box">
+<summary>Abstract</summary>
+<blockquote>
+<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 class="box" 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 the
+COPYING file included in both of
+the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> source
+archives linked above.</p>
+
+<h3 id="presentation">Presentation</h3>
+
+<p>Reference version:
+pdf (coming soon)<br />
+<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> 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="https://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>
+
+<hr />
+<details id="copy">
+<summary>Copyright © 2020 bandali</summary>
+<p>Copying and distribution of this file, with or without
+modification, are permitted in any medium without royalty provided the
+copyright notice and this notice are preserved. This file is offered
+as-is, without any warranty.</p>
+</details>
+</body>
+</html>