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

   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 &mdash; 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 &lt;<a href="https://www.gnu.org/licenses/">https://www.gnu.org/licenses/</a>&gt;.
 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 &copy; 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>