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

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