Show simple item record

dc.contributor.authorBandali, Amin 20:10:14 (GMT) 20:10:14 (GMT)
dc.description.abstractDeclarative 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.en
dc.publisherUniversity of Waterlooen
dc.subjectformal methodsen
dc.subjectmodel checkingen
dc.subjectdeclarative modellingen
dc.subjectdeclarative modelling languagesen
dc.titleA Comprehensive Study of Declarative Modelling Languagesen
dc.typeMaster Thesisen
dc.pendingfalse R. Cheriton School of Computer Scienceen Scienceen of Waterlooen
uws-etd.degreeMaster of Mathematicsen
uws.contributor.advisorDay, Nancy
uws.contributor.affiliation1Faculty of Mathematicsen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages