X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/9097e885c91d4c051502d9fe82972eb98f83ea93..dadecbb05c6be35c7fdab9c46118ae8e2510c1ff:/mmath.html diff --git a/mmath.html b/mmath.html deleted file mode 100644 index 1c7fc59..0000000 --- a/mmath.html +++ /dev/null @@ -1,172 +0,0 @@ -<!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="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">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 <<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 /> -<details id="copy"> -<summary>Copyright © 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>