smallish spelling fixes
[~bandali/bndl.org] / mmath.html
CommitLineData
7b376474
AB
1<!doctype html>
2<html lang="en">
3<head>
4<meta charset="utf-8" />
5<meta name="author" content="bandali" />
6<meta name="viewport" content="width=device-width, initial-scale=1" />
7<title>master of mathematics &mdash; bandali</title>
8<link rel="canonical" href="https://bndl.org/mmath.html" />
9<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
10<style>
11body {
12 line-height: 1.6;
13 max-width: 37.5em;
14 margin: 0 auto;
15 padding: 0 1em;
16}
17details { margin: 1em 0; }
18details summary { cursor: pointer; }
19#copy { font-size: 0.84em; }
20#copy p { padding: 0 2em; }
21blockquote { text-align: justify; }
22.tex {
23 font-family: "Tex Gyre Termes", serif;
24 text-transform: uppercase;
25}
26.tex sub {
27 font-size: 1em;
28 margin-left: -0.1667em;
29 margin-right: -0.125em;
30 vertical-align: -0.5ex;
31}
32.tex sup {
33 font-size: 0.85em;
34 margin-left: -0.36em;
35 margin-right: -0.15em;
36 vertical-align: 0.15em;
37}
38.box {
39 background: #f8f8f8;
40 border: 1px solid #e6e6e6;
41 border-radius: 4px;
42 font-size: 0.95em;
43 padding: 0.6em 0.9em;
44}
45@media (prefers-color-scheme: dark) {
46 body { background: #1c1c1c; color: white; }
47 a:link { color: #acdeff; }
48 a:visited { color: #f8f; }
49 a:active { color: #e00; }
50 .box { background: #1b1d1e; border-color: #373c34; }
51}
52</style>
53</head>
54<body>
55<h1><a href=".">bandali</a>'s master of mathematics</h1>
56
57<p>I graduated from the University of Waterloo with the degree of
58Master of Mathematics in Computer Science in Spring 2020. My research
59at the <a href="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
60group focused on formal logic, model checking, and verification; under
61supervision of
62<a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy Day</a>.</p>
eb1aab37
AB
63
64<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
7b376474
AB
65
66<!-- <p><em>Jump to:</em>
67<a href="#thesis">thesis</a> |
68<a href="#presentation">presentation</a> |
69<a href="#models">models</a></p> -->
eb1aab37
AB
70
71<h3 id="thesis">Thesis</h3>
72
73<p>Reference version:
7b376474 74<a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
2b680c48 75<a href="bandali.bib">bib</a><br />
eb1aab37 76
7b376474
AB
77<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
78<a href="https://p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
79<a href="https://p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
80
81<details class="box">
573bd43b 82<summary>Abstract</summary>
7b376474 83<blockquote>
eb1aab37
AB
84<p>Declarative behavioural modelling is a powerful modelling paradigm
85that enables users to model system functionality abstractly and
86formally. An abstract model is a concise and compact representation
87of key characteristics of a system, and enables the stakeholders to
88reason about the correctness of the system in the early stages of
89development.</p>
90
91<p>There are many different declarative languages and they have
92greatly varying constructs for representing a transition system, and
93they sometimes differ in rather subtle ways. In this thesis, we
94compare seven formal declarative modelling languages B, Event-B,
95Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
96criteria. We classify these criteria under three main categories:
97structuring transition systems (control modelling), data descriptions
98in transition systems (data modelling), and modularity aspects of
99modelling. We developed this comparison by completing a set of case
100studies across the data- vs. control-oriented spectrum in all of the
101above languages.</p>
102
103<p>Structurally, a transition system is comprised of a snapshot
104declaration and snapshot space, initialization, and a transition
7b376474
AB
105relation, which is potentially composed of individual transitions.
106We meticulously outline the differences between the languages with
eb1aab37
AB
107respect to how the modeller would express each of the above components
108of a transition system in each language, and include discussions
109regarding stuttering and inconsistencies in the transition relation.
110Data-related aspects of a formal model include use of basic and
111composite datatypes, well-formedness and typechecking, and separation
112of name spaces with respect to global and local variables. Modularity
7b376474
AB
113criteria includes subtransition systems and data decomposition.
114We employ a series of small and concise exemplars we have devised to
eb1aab37
AB
115highlight these differences in each language. To help modellers
116answer the important question of which declarative modelling language
117may be most suited for modelling their system, we present
118recommendations based on our observations about the differentiating
119characteristics of each of these languages.</p>
120</blockquote>
573bd43b 121</details>
eb1aab37 122
7b376474 123<details class="box" open>
573bd43b 124<summary>License</summary>
fcc5b13a
AB
125<pre>
126This thesis is free software: you can redistribute it and/or modify
127it under the terms of the GNU General Public License as published by
128the Free Software Foundation, either version 3 of the License, or
129(at your option) any later version.
130
131This thesis is distributed in the hope that it will be useful,
132but WITHOUT ANY WARRANTY; without even the implied warranty of
133MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
134GNU General Public License for more details.
135
136You should have received a copy of the GNU General Public License
137along with this thesis. If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
138</pre>
573bd43b 139</details>
fcc5b13a 140
7b376474
AB
141<p>A copy of the GNU General Public License is available from the
142COPYING file included in both of
143the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> source
fcc5b13a
AB
144archives linked above.</p>
145
eb1aab37
AB
146<h3 id="presentation">Presentation</h3>
147
148<p>Reference version:
a0e46d57 149pdf (coming soon)<br />
7b376474 150<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
fcc5b13a 151tar.gz | zip (coming soon)</p>
eb1aab37
AB
152
153<p>This is the presentation I delivered to my supervisor and the
154second readers of my thesis on Jun 30, 2020, as
7b376474 155<a href="https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
eb1aab37
AB
156on the Cheriton School of Computer Science website.</p>
157
158<h3 id="models">Models</h3>
159
160<p>Reference version:
fcc5b13a 161tar.gz | zip (coming soon)</p>
eb1aab37 162
7b376474
AB
163<hr />
164<details id="copy">
165<summary>Copyright &copy; 2020 bandali</summary>
166<p>Copying and distribution of this file, with or without
167modification, are permitted in any medium without royalty provided the
168copyright notice and this notice are preserved. This file is offered
169as-is, without any warranty.</p>
170</details>
171</body>
172</html>