--- /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