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