Show simple item record

dc.contributor.authorEid, Elias 19:07:18 (GMT) 19:07:18 (GMT)
dc.description.abstractModeling of software-intensive systems using formal declarative modeling languages offers a means of managing software complexity through the use of abstraction and early identification of correctness issues by formal analysis. Alloy is one such language used for modeling systems early in the development process. Nevertheless, little work has been done to study the styles and techniques commonly used in Alloy models. We present the first static analysis study of Alloy models. We investigate research questions that examine a large corpus of 2,138 Alloy models. To evaluate these research questions, we create a methodology that leverages the power of ANTLR pattern matching and the query language XPath. We investigate the parse tree generated from each Alloy model and identify instances of formulated queries that are of interest to our research questions. We present the results and discuss the findings from examining these research questions. Our research questions are split into three categories depending on their purpose and implementation complexity. Characteristics of Models include ``surface-level" research questions that aim to identify what language constructs are used commonly. We also correlate certain model features using linear regression to determine the best predictors for model length and field count. Patterns of Use questions are considerably more complex and attempt to identify how modelers are using Alloy's constructs. Analysis Complexity questions explore the use of Alloy model features and constructs that may impact solving time. We draw conclusions from the results of our research questions and present findings for language and tool designers, educators and optimization developers. Findings aimed at language and tool designers present ways to improve the Alloy language by adding constructs or removing unused ones based on trends identified in our corpus of models. Findings for educators are intended to highlight underutilized language constructs and features, and help student modelers avoid discouraged practices. Lastly, we present a number of findings for optimization developers that provide suggestions for back-end improvements.en
dc.publisherUniversity of Waterlooen
dc.subjectalloy profilingen
dc.subjectempirical studyen
dc.subjectsoftware modelingen
dc.subjectstatic analysisen
dc.titleProfiling Alloy Modelsen
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