| 1 | bandali's master of mathematics |
| 2 | ------------------------------- |
| 3 | |
| 4 | I graduated from the University of Waterloo with the degree of Master |
| 5 | of Mathematics in Computer Science in Spring 2020. My research at the |
| 6 | Waterloo Formal Methods group focused on formal logic, model checking, |
| 7 | and verification; under supervision of Prof. Nancy Day. |
| 8 | |
| 9 | |
| 10 | A Comprehensive Study of Declarative Modelling Languages |
| 11 | |
| 12 | THESIS |
| 13 | |
| 14 | Reference version: |
| 15 | - https://bndl.org/theses/bandali-mmath-thesis.pdf |
| 16 | LaTeX sources: |
| 17 | - https://bndl.org/theses/bandali-mmath-thesis.tar.gz |
| 18 | - https://bndl.org/theses/bandali-mmath-thesis.zip |
| 19 | |
| 20 | Abstract: |
| 21 | |
| 22 | Declarative behavioural modelling is a powerful modelling paradigm |
| 23 | that enables users to model system functionality abstractly and |
| 24 | formally. An abstract model is a concise and compact |
| 25 | representation of key characteristics of a system, and enables the |
| 26 | stakeholders to reason about the correctness of the system in the |
| 27 | early stages of development. |
| 28 | |
| 29 | There are many different declarative languages and they have |
| 30 | greatly varying constructs for representing a transition system, |
| 31 | and they sometimes differ in rather subtle ways. In this thesis, |
| 32 | we compare seven formal declarative modelling languages B, |
| 33 | Event-B, Alloy, Dash, TLA+, PlusCal, and AsmetaL on several |
| 34 | criteria. We classify these criteria under three main categories: |
| 35 | structuring transition systems (control modelling), data |
| 36 | descriptions in transition systems (data modelling), and |
| 37 | modularity aspects of modelling. We developed this comparison by |
| 38 | completing a set of case studies across the data- |
| 39 | vs. control-oriented spectrum in all of the above languages. |
| 40 | |
| 41 | Structurally, a transition system is comprised of a snapshot |
| 42 | declaration and snapshot space, initialization, and a transition |
| 43 | relation, which is potentially composed of individual transitions. |
| 44 | We meticulously outline the differences between the languages with |
| 45 | respect to how the modeller would express each of the above |
| 46 | components of a transition system in each language, and include |
| 47 | discussions regarding stuttering and inconsistencies in the |
| 48 | transition relation. Data-related aspects of a formal model |
| 49 | include use of basic and composite datatypes, well-formedness and |
| 50 | typechecking, and separation of name spaces with respect to global |
| 51 | and local variables. Modularity criteria includes subtransition |
| 52 | systems and data decomposition. We employ a series of small and |
| 53 | concise exemplars we have devised to highlight these differences |
| 54 | in each language. To help modellers answer the important question |
| 55 | of which declarative modelling language may be most suited for |
| 56 | modelling their system, we present recommendations based on our |
| 57 | observations about the differentiating characteristics of each of |
| 58 | these languages. |
| 59 | |
| 60 | License: |
| 61 | |
| 62 | This thesis is free software: you can redistribute it and/or |
| 63 | modify it under the terms of the GNU General Public License as |
| 64 | published by the Free Software Foundation, either version 3 of |
| 65 | the License, or (at your option) any later version. |
| 66 | |
| 67 | This thesis is distributed in the hope that it will be useful, |
| 68 | but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 69 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 70 | GNU General Public License for more details. |
| 71 | |
| 72 | You should have received a copy of the GNU General Public License |
| 73 | along with this thesis. If not, see |
| 74 | <https://www.gnu.org/licenses/>. |
| 75 | |
| 76 | A copy of the GNU General Public License is available from the |
| 77 | COPYING file included in both of the LaTeX source archives linked |
| 78 | above. |
| 79 | |
| 80 | PRESENTATION |
| 81 | |
| 82 | Reference version: (coming soon) |
| 83 | LaTeX sources: (coming soon) |
| 84 | |
| 85 | This is the presentation I delivered to my supervisor and the second |
| 86 | readers of my thesis on Jun 30, 2020, as announced on the Cheriton |
| 87 | School of Computer Science website: |
| 88 | |
| 89 | https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages |
| 90 | |
| 91 | MODELS |
| 92 | |
| 93 | Reference version: (coming soon) |
| 94 | |
| 95 | |
| 96 | -*- |
| 97 | |
| 98 | Copyright (c) 2020 bandali |
| 99 | |
| 100 | Copying and distribution of this file, with or without modification, |
| 101 | are permitted in any medium without royalty provided the copyright |
| 102 | notice and this notice are preserved. This file is offered as-is, |
| 103 | without any warranty. |
| 104 | |
| 105 | plain text: https://bndl.org/theses/bandali-mmath.txt |