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