use bandali-bib#bandali2020 instead of a bib file
[~bandali/bndl.org] / mmath.m4
CommitLineData
eb1aab37
AB
1dnl -*- html -*-
2define(__title, `Master of Mathematics')dnl
3define(__slug, `mmath')dnl
4include(header.html)dnl
fcc5b13a 5define(__latex, `<span class="t-logo">L<sup>a</sup>T<sub>e</sub>X</span>')dnl
eb1aab37
AB
6
7<article>
8<h1>Master of Mathematics</h1>
9
fcc5b13a
AB
10<p class="justify">I graduated from the University of Waterloo with
11the degree of Master of Mathematics in Computer Science in Spring
122020. My research at the <a href="//watform.uwaterloo.ca">Waterloo
13Formal Methods</a> group focused on formal logic, model checking, and
14verification; under supervision of
15<a href="//cs.uwaterloo.ca/~nday/">Dr. Nancy Day</a>.</p>
eb1aab37
AB
16
17<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
fcc5b13a
AB
18dnl
19dnl<p><em>Jump to:</em>
20dnl<a href="#thesis">thesis</a> |
21dnl<a href="#presentation">presentation</a> |
22dnl<a href="#models">models</a></p>
eb1aab37
AB
23
24<h3 id="thesis">Thesis</h3>
25
26<p>Reference version:
27<a href="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
be86a872 28<a href="bandali-bib#bandali2020">bib</a><br/>
fcc5b13a
AB
29__latex sources:
30<a href="//p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
31<a href="//p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
eb1aab37
AB
32
33<h4 class="center-text">Abstract</h4>
34<blockquote id="abstract">
35<p>Declarative behavioural modelling is a powerful modelling paradigm
36that enables users to model system functionality abstractly and
37formally. An abstract model is a concise and compact representation
38of key characteristics of a system, and enables the stakeholders to
39reason about the correctness of the system in the early stages of
40development.</p>
41
42<p>There are many different declarative languages and they have
43greatly varying constructs for representing a transition system, and
44they sometimes differ in rather subtle ways. In this thesis, we
45compare seven formal declarative modelling languages B, Event-B,
46Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
47criteria. We classify these criteria under three main categories:
48structuring transition systems (control modelling), data descriptions
49in transition systems (data modelling), and modularity aspects of
50modelling. We developed this comparison by completing a set of case
51studies across the data- vs. control-oriented spectrum in all of the
52above languages.</p>
53
54<p>Structurally, a transition system is comprised of a snapshot
55declaration and snapshot space, initialization, and a transition
56relation, which is potentially composed of individual transitions. We
57meticulously outline the differences between the languages with
58respect to how the modeller would express each of the above components
59of a transition system in each language, and include discussions
60regarding stuttering and inconsistencies in the transition relation.
61Data-related aspects of a formal model include use of basic and
62composite datatypes, well-formedness and typechecking, and separation
63of name spaces with respect to global and local variables. Modularity
64criteria includes subtransition systems and data decomposition. We
65employ a series of small and concise exemplars we have devised to
66highlight these differences in each language. To help modellers
67answer the important question of which declarative modelling language
68may be most suited for modelling their system, we present
69recommendations based on our observations about the differentiating
70characteristics of each of these languages.</p>
71</blockquote>
72
fcc5b13a
AB
73<h4>License</h4>
74
75<pre>
76This thesis is free software: you can redistribute it and/or modify
77it under the terms of the GNU General Public License as published by
78the Free Software Foundation, either version 3 of the License, or
79(at your option) any later version.
80
81This thesis is distributed in the hope that it will be useful,
82but WITHOUT ANY WARRANTY; without even the implied warranty of
83MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
84GNU General Public License for more details.
85
86You should have received a copy of the GNU General Public License
87along with this thesis. If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
88</pre>
89
90<p>A copy of the GNU General Public License is available
91from <a href="gpl-3.0.html">gpl-3.0.html</a>, as well as in
92the <code>COPYING</code> file included in both of the __latex source
93archives linked above.</p>
94
eb1aab37
AB
95<h3 id="presentation">Presentation</h3>
96
97<p>Reference version:
98pdf (coming soon)<br/>
fcc5b13a
AB
99__latex sources:
100tar.gz | zip (coming soon)</p>
eb1aab37
AB
101
102<p>This is the presentation I delivered to my supervisor and the
103second readers of my thesis on Jun 30, 2020, as
104<a href="//cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
105on the Cheriton School of Computer Science website.</p>
106
107<h3 id="models">Models</h3>
108
109<p>Reference version:
fcc5b13a 110tar.gz | zip (coming soon)</p>
eb1aab37
AB
111</article>
112
113define(__copy, `2020')dnl
114include(footer.html)dnl