Show simple item record

dc.contributor.authorSerna, Jose 17:19:59 (GMT) 17:19:59 (GMT)
dc.description.abstractAn abstract model is a representation of the fundamental characteristics and properties of a system, and its purpose is to provide feedback to stakeholders about the correctness of the system during the early stages of development. This thesis presents Dash, a new language for the formal specification of abstract behavioural models, which combines the control-oriented constructs of statecharts with the declarative modelling of Alloy. From statecharts, Dash inherits a means to specify hierarchy, concurrency, and communication, three useful aspects to describe the behaviour of reactive systems. From Alloy, Dash uses the expressiveness of relational logic and set theory to abstractly and declaratively describe structures, data, and operations. The purpose of a Dash model is to formally describe a transition system, and for this reason transitions are first-class constructs of the language. Dash provides features such as factoring, transition comprehension, and layering, to systematically declare and organise the transitions of a model. The integration between statecharts and Alloy is done in Dash at the semantic level. The semantics of Dash use the notion of big steps and small steps to formally describe changes in a system, and address the mismatch between declarative and control-oriented formalisms regarding the frame problem. This thesis presents several case studies to demonstrate the modelling capabilities and automated analysis of Dash models. The case studies range from heavily data-oriented systems to highly hierarchical and concurrent systems. Behaviours can be specified using a temporal logic and the Alloy Analyzer is used for performing analyses. We extended the notion of significance axioms and significant scopes to concurrent Dash models, to avoid spurious instances of a model and ensure that a big enough search space is explored by the Analyzer to check for interesting behaviours and provide useful feedback about a model.en
dc.publisherUniversity of Waterlooen
dc.subjectBehavioural modellingen
dc.subjectTransition systemen
dc.titleDash: Declarative Behavioural Modelling in Alloyen
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