X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/7808cfc75162b31f8a0a3fa6c462bea40c82d360..129b56aa7b630d94644398d83c5b2b0e3065005c:/bandali-mmath.txt diff --git a/bandali-mmath.txt b/bandali-mmath.txt deleted file mode 100644 index ebca8b6..0000000 --- a/bandali-mmath.txt +++ /dev/null @@ -1,105 +0,0 @@ -bandali's 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 Prof. Nancy Day. - - - A Comprehensive Study of Declarative Modelling Languages - -THESIS - - Reference version: - - https://p.bndl.org/bandali-mmath-thesis.pdf - LaTeX sources: - - https://p.bndl.org/bandali-mmath-thesis.tar.gz - - https://p.bndl.org/bandali-mmath-thesis.zip - - 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. - - License: - - This thesis is free software: you can redistribute it and/or - modify it under the terms of the GNU General Public License as - published by the Free Software Foundation, either version 3 of - the License, or (at your option) any later version. - - This thesis is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this thesis. If not, see - . - - A copy of the GNU General Public License is available from the - COPYING file included in both of the LaTeX source archives linked - above. - -PRESENTATION - - Reference version: (coming soon) - LaTeX sources: (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: - - https://cs.uwaterloo.ca/events/masters-thesis-presentation-formal-methods-comprehensive-study-declarative-modelling-languages - -MODELS - - Reference version: (coming soon) - - - -*- - -Copyright (c) 2020 bandali - -Copying and distribution of this file, with or without modification, -are permitted in any medium without royalty provided the copyright -notice and this notice are preserved. This file is offered as-is, -without any warranty. - -plain text: https://bndl.org/bandali-mmath.txt