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[1] group focused on
formal logic, model checking, and verification; under supervision
of Prof. Nancy Day[2].

    A Comprehensive Study of Declarative Modelling Languages

Thesis
------

Reference version: pdf[3] | bib[4]
LaTeX sources: tar.gz[5] | zip[6]

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, and also the COPYING.GPL[7] file on this site.

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[8].

Models
------

Reference version: (coming soon)

[1] https://watform.uwaterloo.ca
[2] https://cs.uwaterloo.ca/~nday/
[3] https://kelar.org/~bandali/theses/bandali-mmath-thesis.pdf
   gopher://kelar.org/d/~bandali/theses/bandali-mmath-thesis.pdf
[4] https://kelar.org/~bandali/theses/bandali-mmath-thesis.bib
   gopher://kelar.org/0/~bandali/theses/bandali-mmath-thesis.bib
[5] https://kelar.org/~bandali/theses/bandali-mmath-thesis.tar.gz
   gopher://kelar.org/5/~bandali/theses/bandali-mmath-thesis.tar.gz
[6] https://kelar.org/~bandali/theses/bandali-mmath-thesis.zip
   gopher://kelar.org/5/~bandali/theses/bandali-mmath-thesis.zip
[7] https://kelar.org/~bandali/COPYING.GPL
   gopher://kelar.org/0/~bandali/COPYING.GPL
[8] https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages

Copyright (c) 2020 Amin Bandali.  This work is licensed under
GNU GPLv3+.

You are viewing proxied material from kelar.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.