Simplifying the Analysis of Software Design Variants with a Colorful Alloy

  • Chong Liu
  • Nuno MacedoEmail author
  • Alcino Cunha
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11951)


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.


Formal 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.


  1. 1.
    Apel, S., Kästner, C., Lengauer, C.: Language-independent and automated software composition: the featurehouse experience. IEEE Trans. Softw. Eng. 39(1), 63–79 (2013)CrossRefGoogle Scholar
  2. 2.
    Apel, S., Kästner, C.: An overview of feature-oriented software development. J. Object Technol. 8(5), 49–84 (2009)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)CrossRefGoogle Scholar
  5. 5.
    Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with SNIP. Softw. Tools Technol. Transf. 14(5), 589–612 (2012)CrossRefGoogle Scholar
  6. 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
  7. 7.
    Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 422–437. Springer, Heidelberg (2005). Scholar
  8. 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. 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. 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
  11. 11.
    Feigenspan, J., Kästner, C., Apel, S., Liebig, J., Schulze, M., Dachselt, R., Papendieck, M., Leich, T., Saake, G.: Do background colors improve program comprehension in the #ifdef hell? Empirical Softw. Eng. 18(4), 699–745 (2013)CrossRefGoogle Scholar
  12. 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
  13. 13.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRefGoogle Scholar
  14. 14.
    Jackson, D.: Software Abstractions - Logic, Language, and Analysis, Revised edn. MIT Press, Cambridge (2012)Google Scholar
  15. 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
  16. 16.
    Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3), 14:1–14:39 (2012)CrossRefGoogle Scholar
  17. 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
  18. 18.
    Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)CrossRefGoogle Scholar
  19. 19.
    Schaefer, I., Hähnle, R.: Formal methods in software product line engineering. IEEE Comput. 44(2), 82–85 (2011)CrossRefGoogle Scholar
  20. 20.
    Sree-Kumar, A., Planas, E., Clarisó, R.: Analysis of feature models using Alloy: a survey. In: Proceedings of the 7th International Workshop on Formal Methods and Analysis in Software Product Line Engineering (FMSPLE@ETAPS). EPTCS, vol. 206, pp. 46–60 (2016)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.INESC TEC and Universidade do MinhoBragaPortugal

Personalised recommendations