9d41ee2f229349ca23caf8cbb5bdf50f729223ad
[~bandali/bndl.org] / bandali-mmath.txt
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)