Commit | Line | Data |
---|---|---|
7b376474 AB |
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) |