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
Jump to: thesis | presentation | models
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, and also the COPYING.GPL file on this site.
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 30 June 2020, as announced on the Cheriton School of Computer Science website.
Reference version: tar.gz | zip (coming soon)