Write a Blog >>
Fri 16 - Fri 23 October 2020
Wed 21 Oct 2020 15:00 - 15:20 at Room B - B3-Model Analysis and Validation Chair(s): Marsha Chechik

Alloy is a textual modeling language for structures and behaviors of software designs. The Alloy Analyzer provides various analyses making it a popular light-weight formal methods tool. While Alloy models can be analyzed, explored, and tested there is little support for comparing different versions of Alloy models. We believe that these comparisons are crucial when trying to refactor, refine, or extend models. In this work we present an approach for the semantic comparisons of Alloy models. Our pair-wise comparisons include semantic model differencing and the checking of refactoring, refinement, and extension. We enable the semantic comparison of Alloy models by a translation of two versions into a single model that is able to simulate instances of either one or of both version. Semantic differencing and instance computation require only a single analyses of the combined model in the Alloy Analyzer. We implemented our work and evaluated it on over 600 Alloy models from different sources including version histories. Our evaluation examines the cost of semantic comparisons using the Alloy Analyzer.

Wed 21 Oct

Displayed time zone: Eastern Time (US & Canada) change

15:00 - 16:15
B3-Model Analysis and ValidationTechnical Track at Room B
Chair(s): Marsha Chechik University of Toronto, Canada
Semantic Comparisons of Alloy ModelsFT
Technical Track
Jan Oliver Ringert University of Leicester, Syed Waqee Wali University of Leicester, UK
DOI Pre-print
Automated Generation of Consistent Models with Structural and Attribute ConstraintsFT
Technical Track
Oszkár Semeráth Budapest University of Technology and Economics, Aren Babikian McGill University, Anqi Li , Kristóf Marussy , Daniel Varro McGill University / Budapest University of Technology and Economics
Link to publication
mel - Model Extractor Language for Extracting Facts from ModelsFT
Technical Track
Robert Hackman , Joanne M. Atlee University of Waterloo, Finn Hacket Computer Science, University of Waterloo, Michael W. Godfrey University of Waterloo, Canada
Strengthening Validation of Model Behavior through Filmstrip Templates in the tool USEDemo
Technical Track