X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/b77d1ccc75a49d601266c5194e990c829a6f888e..56af22d033482f66966fb7b8edc2bb18f2fec477:/theses/bandali-mmath.txt

diff --git a/theses/bandali-mmath.txt b/theses/bandali-mmath.txt
new file mode 100644
index 0000000..92532d1
--- /dev/null
+++ b/theses/bandali-mmath.txt
@@ -0,0 +1,105 @@
+bandali's master of mathematics
+-------------------------------
+
+I graduated from the University of Waterloo with the degree of Master
+of Mathematics in Computer Science in Spring 2020.  My research at the
+Waterloo Formal Methods group focused on formal logic, model checking,
+and verification; under supervision of Prof. Nancy Day.
+
+
+       A Comprehensive Study of Declarative Modelling Languages
+
+THESIS
+
+  Reference version:
+    - https://bndl.org/theses/bandali-mmath-thesis.pdf
+  LaTeX sources:
+    - https://bndl.org/theses/bandali-mmath-thesis.tar.gz
+    - https://bndl.org/theses/bandali-mmath-thesis.zip
+
+  Abstract:
+
+    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.
+
+    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+, 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.
+
+    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.
+
+  License:
+
+    This thesis is free software: you can redistribute it and/or
+    modify it under the terms of the GNU General Public License as
+    published by the Free Software Foundation, either version 3 of
+    the License, or (at your option) any later version.
+
+    This thesis is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this thesis.  If not, see
+    <https://www.gnu.org/licenses/>.
+
+  A copy of the GNU General Public License is available from the
+  COPYING file included in both of the LaTeX source archives linked
+  above.
+
+PRESENTATION
+
+  Reference version: (coming soon)
+  LaTeX sources: (coming soon)
+
+  This is the presentation I delivered to my supervisor and the second
+  readers of my thesis on Jun 30, 2020, as announced on the Cheriton
+  School of Computer Science website:
+
+  https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages
+
+MODELS
+
+  Reference version: (coming soon)
+
+
+                                 -*-
+
+Copyright (c) 2020 bandali
+
+Copying and distribution of this file, with or without modification,
+are permitted in any medium without royalty provided the copyright
+notice and this notice are preserved.  This file is offered as-is,
+without any warranty.
+
+plain text: https://bndl.org/theses/bandali-mmath.txt