Bibliographic record
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. \n \nWe 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. \n \nOur 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. \n \nWe 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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.000 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.000 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.000 |
| Open science | 0.000 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.001 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one teacher head, not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".