Master of Mathematics
Tue, 30 Jun 2020 12:00:00 -0400

I graduated from the University of Waterloo with the degree of
Master of Mathematics in Computer Science in summer 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] | [hdl][5]\
LaTeX sources: [tar.gz][6] | [zip][7]

**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][8] 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][9]
on the Cheriton School of Computer Science website.

### Models

Reference version: (coming soon)

[1]: https://watform.uwaterloo.ca
[2]: https://cs.uwaterloo.ca/~nday/
[3]: bandali-mmath-thesis.pdf
[4]: bandali-mmath-thesis.bib
[5]: https://hdl.handle.net/10012/16059
[6]: bandali-mmath-thesis.tar.gz
[7]: bandali-mmath-thesis.zip
[8]: COPYING.GPL
[9]: 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+](license.html#gplv3).