From: Amin Bandali Date: Fri, 5 Nov 2021 02:21:57 +0000 (-0400) Subject: make mmath a directory X-Git-Url: https://git.shemshak.org/~bandali/bndl.org/commitdiff_plain/129b56aa7b630d94644398d83c5b2b0e3065005c make mmath a directory --- 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 diff --git a/mmath.html b/mmath.html deleted file mode 100644 index b9dcbea..0000000 --- a/mmath.html +++ /dev/null @@ -1,144 +0,0 @@ - - - - -master of mathematics — bandali - - - - - -

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

- -

Jump to: -thesis | -presentation | -models

- -

Thesis

- -

Reference version: -pdf | -bib
- -LaTeX sources: -tar.gz | -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 <https://www.gnu.org/licenses/>.
-
-
- -

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: -pdf (coming soon)
-LaTeX sources: -tar.gz | zip (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: -tar.gz | zip (coming soon)

- -
-

Copyright © 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.

- - diff --git a/mmath/bandali-mmath.txt b/mmath/bandali-mmath.txt new file mode 100644 index 0000000..ebca8b6 --- /dev/null +++ b/mmath/bandali-mmath.txt @@ -0,0 +1,105 @@ +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 diff --git a/mmath/index.html b/mmath/index.html new file mode 100644 index 0000000..b9dcbea --- /dev/null +++ b/mmath/index.html @@ -0,0 +1,144 @@ + + + + +master of mathematics — bandali + + + + + +

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

+ +

Jump to: +thesis | +presentation | +models

+ +

Thesis

+ +

Reference version: +pdf | +bib
+ +LaTeX sources: +tar.gz | +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 <https://www.gnu.org/licenses/>.
+
+
+ +

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: +pdf (coming soon)
+LaTeX sources: +tar.gz | zip (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: +tar.gz | zip (coming soon)

+ +
+

Copyright © 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.

+ +