X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/blobdiff_plain/a0e46d57508b45f23f360daa9ba6432e2b2f19f5..76b32a1423b69a094d42f50c0a7906bece44fb8e:/bandali-mmath.txt diff --git a/bandali-mmath.txt b/bandali-mmath.txt deleted file mode 100644 index 9d41ee2..0000000 --- a/bandali-mmath.txt +++ /dev/null @@ -1,94 +0,0 @@ -bandali's master of mathematics -https://bndl.org/bandali-mmath.txt - - -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)