Show simple item record

dc.contributor.authorHossain, Tamjid 12:13:31 (GMT) 12:13:31 (GMT)
dc.description.abstractModelling systems abstractly shows great promise to uncover bugs early in system development. The formal language Alloy provides the means of writing constraints abstractly but lacks explicit constructs for describing transition systems. Extensions to Alloy, such as Electrum, DynAlloy, and Dash, provide such constructs. However, still missing are language constructs to describe easily multiple processes with the same behavior (replicated processes) running in parallel as is found in languages such as PlusCal and Promela. We propose extensions to Dash for replicated processes. The result is Dash+: an Alloy language extension for describing transition systems that include both concurrent and hierarchical states and replicated concurrent processes. The processes can communicate via buffers or exchange information through variables and events. The key contributions of our novel approach are: 1) Replicated and non-replicated components can be nested arbitrarily at any level in the state hierarchy 2) Replicated components can exchange information directly without resorting to global variables as is the case in PlusCal and Promela 3) A modeller can abstractly model the topology of the processes (ring, list, etc.) through constraints on the set indexing the processes 4) Buffers can be used to facilitate communication between replicated components Dash+ stays consistent with the semantics of Dash and uses the notion of big steps and small steps to describe changes in the system. The semantics are implemented in a translation to Alloy in a way that accommodates the following model checking options: traces-based model checking, transitive closure-based model checking (TCMC), and Electrum. Our implementation is fully integrated into the Alloy Analyzer. This thesis presents case studies to demonstrate the features of Dash+ in modelling systems with concurrent processes and the benefits that Dash+ offers over existing languages. We check for properties in each of the models in the case studies to demonstrate how different model checking options can be used.en
dc.publisherUniversity of Waterlooen
dc.titleDash+: Extending Alloy with Replicated Processes for Modelling Transition Systemsen
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