[~bandali/bndl.org] / theses / mmath.html

<!doctype html><html lang="en"><head>
<meta charset="utf-8" />
<meta name="author" content="bandali" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>master of mathematics &mdash; bandali</title>
<link rel="icon" href="data:,">
<link rel="canonical" href="https://bndl.org/theses/mmath.html" />
<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
<style>
body{margin:0 auto;max-width:37.5em;}p{line-height:1.6}
h1{font-size:1.5em}h2{font-size:1.2em}h3{font-size:1.1em}
.box{background:#f8f8f8;border:1px solid #e6e6e6;border-radius:4px;
font-size:0.95em;padding:0.6em 0.9em;}
details{margin:1em 0}details summary{cursor:pointer}
blockquote{text-align:justify}
.tex{font-family:"Tex Gyre Termes",serif;text-transform:uppercase;}
.tex span{font-size:0.75em;margin-left:-0.05em;margin-right:-0.20em;}
.tex sub{font-size:1em;margin-left:-0.1667em;margin-right:-0.125em;
vertical-align:-0.5ex;}.tex sup{font-size:0.85em;margin-left:-0.36em;
margin-right:-0.15em;vertical-align:0.15em;}
#copy,#license{font-size:0.84em;line-height:1.3;}
#copy{margin-bottom:0.5em}#license{margin-top:0.5em}
@media(prefers-color-scheme:dark){body{background:#1c1c1c;color:white;}
a:link{color:#acdeff}a:visited{color:#f8f}a:active{color:#e00}
.box{background:#1b1d1e;border-color:#373c34;}}
</style></head>
<body>
<h1><a href="../">bandali</a>'s master of mathematics</h1>

<p>I graduated from the University of Waterloo with the degree of
Master of Mathematics in Computer Science in Spring 2020.
My research at
the <a href="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
group focused on formal logic, model checking, and verification; under
supervision
of <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy Day</a>.</p>


<h2>A Comprehensive Study of Declarative Modelling Languages</h2>

<p><em>Jump to:</em>
<a href="#thesis">thesis</a> |
<a href="#presentation">presentation</a> |
<a href="#models">models</a></p>

<h3 id="thesis">Thesis</h3>

<p>Reference version:
<a href="bandali-mmath-thesis.pdf">pdf</a> |
<a href="../bandali.bib">bib</a><br />

<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
<a href="bandali-mmath-thesis.tar.gz">tar.gz</a> |
<a href="bandali-mmath-thesis.zip">zip</a></p>

<details class="box">
<summary>Abstract</summary>
<blockquote>
<p>Declarative behavioural modelling is a powerful modelling paradigm
that enables users to model system functionality abstractly and
formally.  An abstract model is a concise and compact representation
of key characteristics of a system, and enables the stakeholders to
reason about the correctness of the system in the early stages of
development.</p>

<p>There are many different declarative languages and they have
greatly varying constructs for representing a transition system, and
they sometimes differ in rather subtle ways.  In this thesis, we
compare seven formal declarative modelling languages B, Event-B,
Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
criteria.  We classify these criteria under three main categories:
structuring transition systems (control modelling), data descriptions
in transition systems (data modelling), and modularity aspects of
modelling.  We developed this comparison by completing a set of case
studies across the data- vs. control-oriented spectrum in all of the
above languages.</p>

<p>Structurally, a transition system is comprised of a snapshot
declaration and snapshot space, initialization, and a transition
relation, which is potentially composed of individual transitions.
We meticulously outline the differences between the languages with
respect to how the modeller would express each of the above components
of a transition system in each language, and include discussions
regarding stuttering and inconsistencies in the transition relation.
Data-related aspects of a formal model include use of basic and
composite datatypes, well-formedness and typechecking, and separation
of name spaces with respect to global and local variables.  Modularity
criteria includes subtransition systems and data decomposition.
We employ a series of small and concise exemplars we have devised to
highlight these differences in each language.  To help modellers
answer the important question of which declarative modelling language
may be most suited for modelling their system, we present
recommendations based on our observations about the differentiating
characteristics of each of these languages.</p>
</blockquote>
</details>

<details class="box" open>
<summary>License</summary>
<pre>
This thesis is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This thesis is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this thesis.  If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
</pre>
</details>

<p>A copy of the GNU General Public License is available from the
COPYING file included in both of
the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> source
archives linked above.</p>

<h3 id="presentation">Presentation</h3>

<p>Reference version:
pdf (coming soon)<br />
<span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
tar.gz | zip (coming soon)</p>

<p>This is the presentation I delivered to my supervisor and the
second readers of my thesis on Jun 30, 2020, as
<a href="https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
on the Cheriton School of Computer Science website.</p>

<h3 id="models">Models</h3>

<p>Reference version:
tar.gz | zip (coming soon)</p>

<hr />
<p id="copy">Copyright &copy; 2020 bandali</p>
<p id="license">Copying and distribution of this file, with or without
modification, are permitted in any medium without royalty provided the
copyright notice and this notice are preserved.  This file is offered
as-is, without any warranty.</p>
</body>
</html>
Commit	Line	Data
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 — bandali</title>
	6	<link rel="icon" href="data:,">
56af22d0	7	<link rel="canonical" href="https://bndl.org/theses/mmath.html" />
7808cfc7 AB	8	<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
7808cfc7 AB	9	<style>
ca00a074	10	body{margin:0 auto;max-width:37.5em;}p{line-height:1.6}
6dbc815a	11	h1{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;
	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;}}
	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
	31	Master of Mathematics in Computer Science in Spring 2020.
	32	My research at
	33	the <a href="https://watform.uwaterloo.ca">Waterloo Formal Methods</a>
	34	group focused on formal logic, model checking, and verification; under
	35	supervision
	36	of <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> \|
a974e138 AB	50	<a href="../bandali.bib">bib</a><br />
7808cfc7 AB	51
7808cfc7 AB	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> \|
a974e138 AB	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
	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
	64	development.</p>
	65
	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
	76	above languages.</p>
	77
	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>
	95	</blockquote>
	96	</details>
	97
	98	<details class="box" open>
	99	<summary>License</summary>
	100	<pre>
	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.
	105
	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.
	110
	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>>.
	113	</pre>
	114	</details>
	115
	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>
120
121	<h3 id="presentation">Presentation</h3>
122
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>
127
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>
132
133	<h3 id="models">Models</h3>
134
135	<p>Reference version:
136	tar.gz \| zip (coming soon)</p>
137
138	<hr />
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>
144	</body>
145	</html>