git.shemshak.org - ~bandali/bndl.org/blame_incremental

... / ...

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