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
   6 <article>
   7 <h1>Master of Mathematics</h1>
   8
   9 <p>I graduated from the University of Waterloo with the degree of
  10 Master of Mathematics in Computer Science in Spring 2020.  My research
  11 at the <a href="//watform.uwaterloo.ca">Waterloo Formal Methods</a>
  12 group focused on formal logic, model checking, and verification; under
  13 supervision of
  14 <a href="//cs.uwaterloo.ca/~nday/">Dr.&nbspNancy&nbsp;A.&nbsp;Day</a>.</p>
  15
  16 <h2>A Comprehensive Study of Declarative Modelling Languages</h2>
  17
  18 <!--<p><em>Jump to:</em>
  19 <a href="#thesis">thesis</a> |
  20 <a href="#presentation">presentation</a> |
  21 <a href="#models">models</a></p>-->
  22
  23 <h3 id="thesis">Thesis</h3>
  24
  25 <p>Reference version:
  26 <a href="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
  27 bib (coming soon)<br/>
  28 LaTeX sources:
  29 zip | tar.gz (coming soon)</p>
  30
  31 <h4 class="center-text">Abstract</h4>
  32 <blockquote id="abstract">
  33 <p>Declarative behavioural modelling is a powerful modelling paradigm
  34 that enables users to model system functionality abstractly and
  35 formally.  An abstract model is a concise and compact representation
  36 of key characteristics of a system, and enables the stakeholders to
  37 reason about the correctness of the system in the early stages of
  38 development.</p>
  39
  40 <p>There are many different declarative languages and they have
  41 greatly varying constructs for representing a transition system, and
  42 they sometimes differ in rather subtle ways.  In this thesis, we
  43 compare seven formal declarative modelling languages B, Event-B,
  44 Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
  45 criteria.  We classify these criteria under three main categories:
  46 structuring transition systems (control modelling), data descriptions
  47 in transition systems (data modelling), and modularity aspects of
  48 modelling.  We developed this comparison by completing a set of case
  49 studies across the data- vs. control-oriented spectrum in all of the
  50 above languages.</p>
  51
  52 <p>Structurally, a transition system is comprised of a snapshot
  53 declaration and snapshot space, initialization, and a transition
  54 relation, which is potentially composed of individual transitions.  We
  55 meticulously outline the differences between the languages with
  56 respect to how the modeller would express each of the above components
  57 of a transition system in each language, and include discussions
  58 regarding stuttering and inconsistencies in the transition relation.
  59 Data-related aspects of a formal model include use of basic and
  60 composite datatypes, well-formedness and typechecking, and separation
  61 of name spaces with respect to global and local variables.  Modularity
  62 criteria includes subtransition systems and data decomposition.  We
  63 employ a series of small and concise exemplars we have devised to
  64 highlight these differences in each language.  To help modellers
  65 answer the important question of which declarative modelling language
  66 may be most suited for modelling their system, we present
  67 recommendations based on our observations about the differentiating
  68 characteristics of each of these languages.</p>
  69 </blockquote>
  70
  71 <h3 id="presentation">Presentation</h3>
  72
  73 <p>Reference version:
  74 pdf (coming soon)<br/>
  75 LaTeX sources:
  76 zip | tar.gz (coming soon)</p>
  77
  78 <p>This is the presentation I delivered to my supervisor and the
  79 second readers of my thesis on Jun 30, 2020, as
  80 <a href="//cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
  81 on the Cheriton School of Computer Science website.</p>
  82
  83 <h3 id="models">Models</h3>
  84
  85 <p>Reference version:
  86 zip | tar.gz (coming soon)</p>
  87 </article>
  88
  89 define(__copy, `2020')dnl
  90 include(footer.html)dnl