From: Amin Bandali Date: Fri, 10 Jul 2020 04:22:01 +0000 (-0400) Subject: add mmath page (wip) X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/commitdiff_plain/eb1aab372e720aaf68aef33d49f8b80950ff566c?hp=3fdab855a4dd23026c0320dbb01a58acbfd7c728 add mmath page (wip) --- diff --git a/mmath.m4 b/mmath.m4 new file mode 100644 index 0000000..28c4138 --- /dev/null +++ b/mmath.m4 @@ -0,0 +1,90 @@ +dnl -*- html -*- +define(__title, `Master of Mathematics')dnl +define(__slug, `mmath')dnl +include(header.html)dnl + +
+

Master of Mathematics

+ +

I graduated from the University of Waterloo with the degree of +Master of Mathematics in Computer Science in Spring 2020. My research +at the Waterloo Formal Methods +group focused on formal logic, model checking, and verification; under +supervision of +Dr. Nancy A. Day.

+ +

A Comprehensive Study of Declarative Modelling Languages

+ + + +

Thesis

+ +

Reference version: +pdf | +bib (coming soon)
+LaTeX sources: +zip | tar.gz (coming soon)

+ +

Abstract

+
+

Declarative behavioural modelling is a powerful modelling paradigm +that enables users to model system functionality abstractly and +formally. An abstract model is a concise and compact representation +of key characteristics of a system, and enables the stakeholders to +reason about the correctness of the system in the early stages of +development.

+ +

There are many different declarative languages and they have +greatly varying constructs for representing a transition system, and +they sometimes differ in rather subtle ways. In this thesis, we +compare seven formal declarative modelling languages B, Event-B, +Alloy, Dash, TLA+, PlusCal, and AsmetaL on several +criteria. We classify these criteria under three main categories: +structuring transition systems (control modelling), data descriptions +in transition systems (data modelling), and modularity aspects of +modelling. We developed this comparison by completing a set of case +studies across the data- vs. control-oriented spectrum in all of the +above languages.

+ +

Structurally, a transition system is comprised of a snapshot +declaration and snapshot space, initialization, and a transition +relation, which is potentially composed of individual transitions. We +meticulously outline the differences between the languages with +respect to how the modeller would express each of the above components +of a transition system in each language, and include discussions +regarding stuttering and inconsistencies in the transition relation. +Data-related aspects of a formal model include use of basic and +composite datatypes, well-formedness and typechecking, and separation +of name spaces with respect to global and local variables. Modularity +criteria includes subtransition systems and data decomposition. We +employ a series of small and concise exemplars we have devised to +highlight these differences in each language. To help modellers +answer the important question of which declarative modelling language +may be most suited for modelling their system, we present +recommendations based on our observations about the differentiating +characteristics of each of these languages.

+
+ +

Presentation

+ +

Reference version: +pdf (coming soon)
+LaTeX sources: +zip | tar.gz (coming soon)

+ +

This is the presentation I delivered to my supervisor and the +second readers of my thesis on Jun 30, 2020, as +announced +on the Cheriton School of Computer Science website.

+ +

Models

+ +

Reference version: +zip | tar.gz (coming soon)

+
+ +define(__copy, `2020')dnl +include(footer.html)dnl diff --git a/static/style.css b/static/style.css index 8d43f66..6270036 100644 --- a/static/style.css +++ b/static/style.css @@ -101,6 +101,15 @@ article h3 { bottom: 0.05em; } +.center-text { + text-align: center; +} + +blockquote#abstract { + font-size: 0.95em; + text-align: justify; +} + pre, code { background: #f6f6f6; font: 1.15em monospace;