Commit | Line | Data |
---|---|---|
7b376474 | 1 | bandali's master of mathematics |
d3adcff4 | 2 | ------------------------------- |
7b376474 AB |
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: | |
56af22d0 | 15 | - https://bndl.org/theses/bandali-mmath-thesis.pdf |
7b376474 | 16 | LaTeX sources: |
56af22d0 AB |
17 | - https://bndl.org/theses/bandali-mmath-thesis.tar.gz |
18 | - https://bndl.org/theses/bandali-mmath-thesis.zip | |
7b376474 AB |
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) | |
d3adcff4 AB |
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 | ||
56af22d0 | 105 | plain text: https://bndl.org/theses/bandali-mmath.txt |