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://p.bndl.org/bandali-mmath-thesis.pdf
  LaTeX sources:
    - https://p.bndl.org/bandali-mmath-thesis.tar.gz
    - https://p.bndl.org/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/bandali-mmath.txt