FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023
Sun 14 May 2023 14:45 - 15:15 at Meeting Room 102 - Specification Chair(s): Larissa A. Meinicke

Alloy is a declarative formal modeling language with syntax derived from notations common to object-oriented design and a first-order relational logic semantics. To better understand the usability of Alloy, the paper presents the results of an empirical study with 30 participants assessing two types of modeling tasks: bug fixing and model building based on natural language specifications. The participants consisted of both novices and non-novices. Besides accuracy and time to complete tasks, we also examined the correlation between the performance of two cognitive tasks (mental rotation and operation span) and task performance. Results indicate that overall non-novices completed the tasks with significantly higher accuracy (54% more accurate) than novices. In the novice group, performing more actions using the Alloy analyzer led to more edits and, eventually higher scores in bug fixing tasks. We found that participants of all levels had much difficulty writing a model from scratch, and they did not utilize the analyzer to improve their models. On average, non-novices completed all the tasks 32 minutes faster than novices. Non-novices who performed better on the Alloy tasks had higher mental rotation scores, which indicates the importance of spatial cognition ability in solving Alloy tasks. Overall, we find that there is a definite need for improving the usability of the visualizations in Alloy Analyzer. We discuss the implications of these findings.

Sun 14 May

Displayed time zone: Hobart change

13:45 - 15:15
SpecificationFormaliSE 2023 at Meeting Room 102
Chair(s): Larissa A. Meinicke The University of Queensland
13:45
30m
Paper
Contract-Based Specification Refinement and Repair for Mission Planning
FormaliSE 2023
Piergiuseppe Mallozzi UC Berkeley, Inigo Incer University of California, Berkeley, Pierluigi Nuzzo University of Southern California, Alberto L. Sangiovanni-Vincentelli University of California at Berkeley, USA
14:15
30m
Paper
Patch Specifications via Product Programs
FormaliSE 2023
Cristian Cadar Imperial College London, UK, Daniel Schemmel Imperial College London, Arindam Sharma Imperial College London
14:45
30m
Paper
An Empirical Study Assessing Software Modeling in Alloy
FormaliSE 2023
Niloofar Mansoor University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln, Eunsuk Kang Carnegie Mellon University, Bonita Sharif University of Nebraska-Lincoln, USA