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