Simplifying the analysis of software design variants with a colorful Alloy

By Chong Liu, INESC TEC

Formal modeling and automatic analysis are essential to achieve a trustworthy software design prior to its implementation. Alloy and its Analyzer are a popular language and tool for this task. Frequently, rather than a single software artifact, the goal is to develop a full software product line (SPL) with many variants supporting different features. Ideally, software design languages and tools should provide support for analyzing all such variants (e.g., by helping pinpoint combinations of features that could break a property), but that is not currently the case. Even when developing a single artifact, support for multi-variant analysis is desirable to explore design alternatives. Several techniques have been proposed to simplify the implementation of SPLs. One such technique is to use background colors to identify the fragments of code associated with each feature. In this paper we propose to use that same technique for formal design, showing how to add support for features and background colors to Alloy and its Analyzer, thus easing the analysis of software design variants. Some illustrative examples and evaluation results are presented, showing the benefits and efficiency of the implemented technique. 

About the Speaker:
Chong Liu is currently a PhD student supervised by Prof.Alcino and Prof. Nuno Macedo at the MAP-i Doctoral Program in Computer Science held by the Universities of Minho, Porto, and Aveiro, Portugal.  She is a researcher at HASLab, INESC TEC & University of Minho. Her research interests lie in formal methods and feature-oriented design. She is particularly interested in high-level software design under variability. Currently, she focusing on Alloy, a lightweight specification framework for verifying first-order properties of structural designs specified at a high level of abstraction, in order to support high-level design under variability. She holds an MSc degree in Engineering of Computer Networks and Telematic Service from the University of Minho, and an MSc degree in Software Engineering from Jilin University, China.


Address:  University of Minho, Gualtar Campus, Braga, Portugal

Building: Departamento de Informatica, Building 07

Networking Session: 01:45 PM, Auditorium A1, Ground floor

Talk Session: 02:00 PM, Auditorium A1, Ground floor