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