X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/7b376474f6dabd5bd525d49b5d333fa18c8e897a..a974e138a0e59afd40a7c31821ab70c3285cf7b8:/mmath.html diff --git a/mmath.html b/mmath.html deleted file mode 100644 index e187918..0000000 --- a/mmath.html +++ /dev/null @@ -1,172 +0,0 @@ - - - - - - -master of mathematics — bandali - - - - - -

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: -pdf | -bib
- -LaTeX sources: -tar.gz | -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: -pdf (coming soon)
-LaTeX sources: -tar.gz | zip (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.

- -

Models

- -

Reference version: -tar.gz | zip (coming soon)

- -
-
-Copyright © 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.

-
- -