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