Towards User-Friendly and Efficient Analysis with Alloy

Abstract—In model-driven engineering, structural models represent software at the early phases of software development. They are assumed to generate the models in subsequent phases which finally result in software. Thus, it is important to make sure these models are correct w.r.t. different concerns, e.g., consistency, or lack of redundant constraints. In this paper, we present a bounded verification approach using Alloy and integrate it into a graphical modelling tool. The graphical models and the properties to be verified are automatically transformed to Alloy specifications, which are examined by the Alloy Analyzer to verify whether the models satisfy the properties. The verification results are presented as feedbacks in the modelling tool. In this way, a model designer can verify models without knowing the underlying verification techniques and receive user-friendly feedbacks. A challenge in the verification approach is scalability. To tackle this, we present a technique f...

• Type: Journal
• Year: 2015
• Where: MODELS
• Authors: Xiaoliang Wang, Adrian Rutle, Yngve Lamo
• Keywords: MODELS 2015, Natural Language Processing