+++ /dev/null
-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
projects / ~bandali / bndl.org / blobdiff