From eb1aab372e720aaf68aef33d49f8b80950ff566c Mon Sep 17 00:00:00 2001
From: Amin Bandali <bandali@gnu.org>
Date: Fri, 10 Jul 2020 00:22:01 -0400
Subject: [PATCH] add mmath page (wip)

---
 mmath.m4         | 90 ++++++++++++++++++++++++++++++++++++++++++++++++
 static/style.css |  9 +++++
 2 files changed, 99 insertions(+)
 create mode 100644 mmath.m4

diff --git a/mmath.m4 b/mmath.m4
new file mode 100644
index 0000000..28c4138
--- /dev/null
+++ b/mmath.m4
@@ -0,0 +1,90 @@
+dnl -*- html -*-
+define(__title, `Master of Mathematics')dnl
+define(__slug, `mmath')dnl
+include(header.html)dnl
+
+<article>
+<h1>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="//watform.uwaterloo.ca">Waterloo Formal Methods</a>
+group focused on formal logic, model checking, and verification; under
+supervision of
+<a href="//cs.uwaterloo.ca/~nday/">Dr.&nbspNancy&nbsp;A.&nbsp;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="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
+bib (coming soon)<br/>
+LaTeX sources:
+zip | tar.gz (coming soon)</p>
+
+<h4 class="center-text">Abstract</h4>
+<blockquote id="abstract">
+<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>
+
+<h3 id="presentation">Presentation</h3>
+
+<p>Reference version:
+pdf (coming soon)<br/>
+LaTeX sources:
+zip | tar.gz (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="//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:
+zip | tar.gz (coming soon)</p>
+</article>
+
+define(__copy, `2020')dnl
+include(footer.html)dnl
diff --git a/static/style.css b/static/style.css
index 8d43f66..6270036 100644
--- a/static/style.css
+++ b/static/style.css
@@ -101,6 +101,15 @@ article h3 {
   bottom: 0.05em;
 }
 
+.center-text {
+  text-align: center;
+}
+
+blockquote#abstract {
+  font-size: 0.95em;
+  text-align: justify;
+}
+
 pre, code {
   background: #f6f6f6;
   font: 1.15em monospace;
-- 
2.20.1