X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/ccd7a4805a0486cb1bf38706c2872be36fb0fc8c..7b376474f6dabd5bd525d49b5d333fa18c8e897a:/mmath.m4 diff --git a/mmath.m4 b/mmath.m4 deleted file mode 100644 index eb6d07d..0000000 --- a/mmath.m4 +++ /dev/null @@ -1,116 +0,0 @@ -dnl -*- html -*- -define(__title, `Master of Mathematics')dnl -define(__slug, `mmath')dnl -include(header.html)dnl - -
-

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

-dnl -dnl

Jump to: -dnlthesis | -dnlpresentation | -dnlmodels

- -

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 gpl-3.0.html, as well as in -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)

-
- -define(__copy, `2020')dnl -include(footer.html)dnl