Profiling Alloy Models

Abstract

Modeling 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.