Simplifying the Analysis of Software Design Variants with a Colorful Alloy
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.
KeywordsFormal software design Variability Alloy
This work is financed by the ERDF - European Regional Development Fund - through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 - and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-016826. The third author was also supported by the FCT sabbatical grant with reference SFRH/BSAB/143106/2018.
- 3.Apel, S., Scholz, W., Lengauer, C., Kästner, C.: Detecting dependences and interactions in feature-oriented design. In: Proceedings of the IEEE 21st International Symposium on Software Reliability Engineering (ISSRE), pp. 151–170. IEEE (2010)Google Scholar
- 6.Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE), pp. 335–344. ACM (2010)Google Scholar
- 8.Czarnecki, K., Pietroszek, K.: Verifying feature-based model templates against well-formedness OCL constraints. In: Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE), pp. 211–220. ACM (2006)Google Scholar
- 9.Czarnecki, K., Wasowski, A.: Feature diagrams and logics: there and back again. In: Proceedings of the 11th International Conference Software Product Lines (SPLC), pp. 23–34. IEEE (2007)Google Scholar
- 10.Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: Proceedings of the 12th International Conference on Software Product Lines (SPLC), pp. 193–202. IEEE (2008)Google Scholar
- 12.Heidenreich, F., Kopcsek, J., Wende, C.: FeatureMapper: mapping features to models. In: Companion Volume of the 30th International Conference on Software Engineering (ICSE Companion), pp. 943–944. ACM (2008)Google Scholar
- 14.Jackson, D.: Software Abstractions - Logic, Language, and Analysis, Revised edn. MIT Press, Cambridge (2012)Google Scholar
- 15.Kästner, C., Apel, S., Kuhlemann, M.: Granularity in software product lines. In: Proceedings of the 30th International Conference on Software Engineering (ICSE), pp. 311–320. ACM (2008)Google Scholar
- 17.Macedo, N., Cunha, A., Pereira, J., Carvalho, R., Silva, R., Paiva, A.C.R., Ramalho, M.S., Silva, D.C.: Sharing and learning Alloy on the web. CoRR abs/1907.02275 (2019)Google Scholar