[~bandali/bndl.org] / 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="canonical" href="https://bndl.org/mmath.html" />
<link rel="alternate" href="bandali-mmath.txt" title="plain text" type="text/plain" />
<style>
body {
  line-height: 1.6;
  max-width: 37.5em;
  margin: 0 auto;
  padding: 0 1em;
}
details { margin: 1em 0; }
details summary { cursor: pointer; }
#copy { font-size: 0.84em; }
#copy p { padding: 0 2em; }
blockquote { text-align: justify; }
.tex {
  font-family: "Tex Gyre Termes", serif;
  text-transform: uppercase;
}
.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;
}
.box {
  background: #f8f8f8;
  border: 1px solid #e6e6e6;
  border-radius: 4px;
  font-size: 0.95em;
  padding: 0.6em 0.9em;
}
@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="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
<a href="bandali-bib.html#bandali2020">bib</a><br/>

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