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.
+ + +Jump to: +thesis | +presentation | +models
+ +Reference version:
+pdf |
+bib
+
+LaTeX sources:
+tar.gz |
+zip
++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.
+
+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.
+ +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.
+ +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.
+ +