git.shemshak.org - ~bandali/bndl.org/blob - mmath.html

   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 &mdash; 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>
  63
  64 <h2>A Comprehensive Study of Declarative Modelling Languages</h2>
  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> -->
  70
  71 <h3 id="thesis">Thesis</h3>
  72
  73 <p>Reference version:
  74 <a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
  75 <a href="bandali-bib.html#bandali2020">bib</a><br />
  76
  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">
  82 <summary>Abstract</summary>
  83 <blockquote>
  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
 105 relation, which is potentially composed of individual transitions.
 106 We meticulously outline the differences between the languages with
 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
 113 criteria includes subtransition systems and data decomposition.
 114 We employ a series of small and concise exemplars we have devised to
 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>
 121 </details>
 122
 123 <details class="box" open>
 124 <summary>License</summary>
 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 &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
 138 </pre>
 139 </details>
 140
 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
 144 archives linked above.</p>
 145
 146 <h3 id="presentation">Presentation</h3>
 147
 148 <p>Reference version:
 149 pdf (coming soon)<br />
 150 <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> sources:
 151 tar.gz | zip (coming soon)</p>
 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
 155 <a href="https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
 156 on the Cheriton School of Computer Science website.</p>
 157
 158 <h3 id="models">Models</h3>
 159
 160 <p>Reference version:
 161 tar.gz | zip (coming soon)</p>
 162
 163 <hr />
 164 <details id="copy">
 165 <summary>Copyright &copy; 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>