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

   1 dnl -*- html -*-
   2 define(__title, `Master of Mathematics')dnl
   3 define(__slug, `mmath')dnl
   4 include(header.html)dnl
   5 define(__latex, `<span class="t-logo">L<sup>a</sup>T<sub>e</sub>X</span>')dnl
   6
   7 <article>
   8 <h1>Master of Mathematics</h1>
   9
  10 <p class="justify">I graduated from the University of Waterloo with
  11 the degree of Master of Mathematics in Computer Science in Spring
  12 2020.  My research at the <a href="//watform.uwaterloo.ca">Waterloo
  13 Formal Methods</a> group focused on formal logic, model checking, and
  14 verification; under supervision of
  15 <a href="//cs.uwaterloo.ca/~nday/">Dr. Nancy Day</a>.</p>
  16
  17 <h2>A Comprehensive Study of Declarative Modelling Languages</h2>
  18 dnl
  19 dnl<p><em>Jump to:</em>
  20 dnl<a href="#thesis">thesis</a> |
  21 dnl<a href="#presentation">presentation</a> |
  22 dnl<a href="#models">models</a></p>
  23
  24 <h3 id="thesis">Thesis</h3>
  25
  26 <p>Reference version:
  27 <a href="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
  28 <a href="bandali-bib#bandali2020">bib</a><br/>
  29 __latex sources:
  30 <a href="//p.bndl.org/bandali-mmath-thesis.tar.gz">tar.gz</a> |
  31 <a href="//p.bndl.org/bandali-mmath-thesis.zip">zip</a></p>
  32
  33 <details>
  34 <summary>Abstract</summary>
  35 <blockquote id="abstract">
  36 <p>Declarative behavioural modelling is a powerful modelling paradigm
  37 that enables users to model system functionality abstractly and
  38 formally.  An abstract model is a concise and compact representation
  39 of key characteristics of a system, and enables the stakeholders to
  40 reason about the correctness of the system in the early stages of
  41 development.</p>
  42
  43 <p>There are many different declarative languages and they have
  44 greatly varying constructs for representing a transition system, and
  45 they sometimes differ in rather subtle ways.  In this thesis, we
  46 compare seven formal declarative modelling languages B, Event-B,
  47 Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
  48 criteria.  We classify these criteria under three main categories:
  49 structuring transition systems (control modelling), data descriptions
  50 in transition systems (data modelling), and modularity aspects of
  51 modelling.  We developed this comparison by completing a set of case
  52 studies across the data- vs. control-oriented spectrum in all of the
  53 above languages.</p>
  54
  55 <p>Structurally, a transition system is comprised of a snapshot
  56 declaration and snapshot space, initialization, and a transition
  57 relation, which is potentially composed of individual transitions.  We
  58 meticulously outline the differences between the languages with
  59 respect to how the modeller would express each of the above components
  60 of a transition system in each language, and include discussions
  61 regarding stuttering and inconsistencies in the transition relation.
  62 Data-related aspects of a formal model include use of basic and
  63 composite datatypes, well-formedness and typechecking, and separation
  64 of name spaces with respect to global and local variables.  Modularity
  65 criteria includes subtransition systems and data decomposition.  We
  66 employ a series of small and concise exemplars we have devised to
  67 highlight these differences in each language.  To help modellers
  68 answer the important question of which declarative modelling language
  69 may be most suited for modelling their system, we present
  70 recommendations based on our observations about the differentiating
  71 characteristics of each of these languages.</p>
  72 </blockquote>
  73 </details>
  74
  75 <details open>
  76 <summary>License</summary>
  77 <pre>
  78 This thesis is free software: you can redistribute it and/or modify
  79 it under the terms of the GNU General Public License as published by
  80 the Free Software Foundation, either version 3 of the License, or
  81 (at your option) any later version.
  82
  83 This thesis is distributed in the hope that it will be useful,
  84 but WITHOUT ANY WARRANTY; without even the implied warranty of
  85 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  86 GNU General Public License for more details.
  87
  88 You should have received a copy of the GNU General Public License
  89 along with this thesis.  If not, see &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
  90 </pre>
  91 </details>
  92
  93 <p>A copy of the GNU General Public License is available
  94 from <a href="gpl-3.0.html">gpl-3.0.html</a>, as well as in
  95 the <code>COPYING</code> file included in both of the __latex source
  96 archives linked above.</p>
  97
  98 <h3 id="presentation">Presentation</h3>
  99
 100 <p>Reference version:
 101 pdf (coming soon)<br/>
 102 __latex sources:
 103 tar.gz | zip (coming soon)</p>
 104
 105 <p>This is the presentation I delivered to my supervisor and the
 106 second readers of my thesis on Jun 30, 2020, as
 107 <a href="//cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
 108 on the Cheriton School of Computer Science website.</p>
 109
 110 <h3 id="models">Models</h3>
 111
 112 <p>Reference version:
 113 tar.gz | zip (coming soon)</p>
 114 </article>
 115
 116 define(__copy, `2020')dnl
 117 include(footer.html)dnl