Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
For a thorough presentation of the Alloy language and the Analyzer, please see [14].
- 3.
We actually force the stripped model to be a valid Alloy model, forbidding, for instance, declarations with the same identifier associated with different feature sets.
- 4.
Function \(\mathsf {arity}\) is an oversimplification, since calculating the arity of a bounding expression requires the arity of other declared sigs and fields.
- 5.
To avoid collisions with the identifiers of the colorful model, the translation actually uses obfuscated identifiers these signatures.
References
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)
Apel, S., Kästner, C.: An overview of feature-oriented software development. J. Object Technol. 8(5), 49–84 (2009)
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)
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)
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)
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)
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). https://doi.org/10.1007/11561347_28
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)
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)
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)
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)
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)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Jackson, D.: Software Abstractions - Logic, Language, and Analysis, Revised edn. MIT Press, Cambridge (2012)
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)
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)
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)
Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)
Schaefer, I., Hähnle, R.: Formal methods in software product line engineering. IEEE Comput. 44(2), 82–85 (2011)
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)
Acknowledgments
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Liu, C., Macedo, N., Cunha, A. (2019). Simplifying the Analysis of Software Design Variants with a Colorful Alloy. In: Guan, N., Katoen, JP., Sun, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2019. Lecture Notes in Computer Science(), vol 11951. Springer, Cham. https://doi.org/10.1007/978-3-030-35540-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-35540-1_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-35539-5
Online ISBN: 978-3-030-35540-1
eBook Packages: Computer ScienceComputer Science (R0)