various updates
[~bandali/bndl.org] / mmath.m4
CommitLineData
eb1aab37
AB
1dnl -*- html -*-
2define(__title, `Master of Mathematics')dnl
3define(__slug, `mmath')dnl
4include(header.html)dnl
5
6<article>
7<h1>Master of Mathematics</h1>
8
9<p>I graduated from the University of Waterloo with the degree of
10Master of Mathematics in Computer Science in Spring 2020. My research
11at the <a href="//watform.uwaterloo.ca">Waterloo Formal Methods</a>
12group focused on formal logic, model checking, and verification; under
13supervision of
14<a href="//cs.uwaterloo.ca/~nday/">Dr.&nbspNancy&nbsp;A.&nbsp;Day</a>.</p>
15
16<h2>A Comprehensive Study of Declarative Modelling Languages</h2>
17
18<!--<p><em>Jump to:</em>
19<a href="#thesis">thesis</a> |
20<a href="#presentation">presentation</a> |
21<a href="#models">models</a></p>-->
22
23<h3 id="thesis">Thesis</h3>
24
25<p>Reference version:
26<a href="//p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
27bib (coming soon)<br/>
28LaTeX sources:
29zip | tar.gz (coming soon)</p>
30
31<h4 class="center-text">Abstract</h4>
32<blockquote id="abstract">
33<p>Declarative behavioural modelling is a powerful modelling paradigm
34that enables users to model system functionality abstractly and
35formally. An abstract model is a concise and compact representation
36of key characteristics of a system, and enables the stakeholders to
37reason about the correctness of the system in the early stages of
38development.</p>
39
40<p>There are many different declarative languages and they have
41greatly varying constructs for representing a transition system, and
42they sometimes differ in rather subtle ways. In this thesis, we
43compare seven formal declarative modelling languages B, Event-B,
44Alloy, Dash, TLA<sup>+</sup>, PlusCal, and AsmetaL on several
45criteria. We classify these criteria under three main categories:
46structuring transition systems (control modelling), data descriptions
47in transition systems (data modelling), and modularity aspects of
48modelling. We developed this comparison by completing a set of case
49studies across the data- vs. control-oriented spectrum in all of the
50above languages.</p>
51
52<p>Structurally, a transition system is comprised of a snapshot
53declaration and snapshot space, initialization, and a transition
54relation, which is potentially composed of individual transitions. We
55meticulously outline the differences between the languages with
56respect to how the modeller would express each of the above components
57of a transition system in each language, and include discussions
58regarding stuttering and inconsistencies in the transition relation.
59Data-related aspects of a formal model include use of basic and
60composite datatypes, well-formedness and typechecking, and separation
61of name spaces with respect to global and local variables. Modularity
62criteria includes subtransition systems and data decomposition. We
63employ a series of small and concise exemplars we have devised to
64highlight these differences in each language. To help modellers
65answer the important question of which declarative modelling language
66may be most suited for modelling their system, we present
67recommendations based on our observations about the differentiating
68characteristics of each of these languages.</p>
69</blockquote>
70
71<h3 id="presentation">Presentation</h3>
72
73<p>Reference version:
74pdf (coming soon)<br/>
75LaTeX sources:
76zip | tar.gz (coming soon)</p>
77
78<p>This is the presentation I delivered to my supervisor and the
79second readers of my thesis on Jun 30, 2020, as
80<a href="//cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages">announced</a>
81on the Cheriton School of Computer Science website.</p>
82
83<h3 id="models">Models</h3>
84
85<p>Reference version:
86zip | tar.gz (coming soon)</p>
87</article>
88
89define(__copy, `2020')dnl
90include(footer.html)dnl