X-Git-Url: https://git.shemshak.org/gitweb.cgi/~bandali/bndl.org/blobdiff_plain/ca00a074941f17e9d5bda7fc5d01c938b629720b..56af22d033482f66966fb7b8edc2bb18f2fec477:/theses/mmath.html diff --git a/theses/mmath.html b/theses/mmath.html new file mode 100644 index 0000000..a9a7682 --- /dev/null +++ b/theses/mmath.html @@ -0,0 +1,145 @@ +<!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 — 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 <<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>>. +</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 © 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>