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