SACS | Faithful Modeling of Product Lines with Kripke Structures and Modal Logic

Published in Volume XXVI, Issue 1, 2016, pages 69-122, doi: 10.7561/SACS.2016.1.69

Authors: Z. Diskin, A. Safilian, T. Maibaum, S. Ben-David

Abstract

Software product lines are now an established framework for software design. They are specified by special diagrams called feature models. For formal analysis, the latter are usually encoded by Boolean propositional theories. We discuss a major deficiency of this semantics, and show that it can be fixed by considering a product to be an instantiation process rather than its final result. We call intermediate states of this process partial products, and argue that what a feature model really defines is a poset of its partial products. We argue that such structures can be viewed as special Kripke structure that we call partial product Kripke structures, ppKS. To specify these Kripke structures, we propose a CTL-based logic, called partial product CTL, ppCTL. We show how to represent a feature model M by a ppCTL theory ML(M) (ML stands for modal logic) such that any ppKS satisfying the theory is equal to the partial product line determined by M. Hence, ML(M) can be considered a sound and complete representation of M. We also discuss several applications of the modal logic view in feature modeling, including refactoring of feature models.

Full Text (PDF)

References

[1] M. Acher, P. Collet, P. Lahire, and R. France. Managing multiple software product lines using merging techniques. University of Nice Sophia Antipolis. TechnicalReport, ISRN I3S/RR, 6, 2010. URL: http://www.i3s.unice.fr/~mh/RR/2010/RR-10-06-P.LAHIRE.pdf

[2] V. Alves, C. Schwanninger, L. Barbosa, A. Rashid, P. Sawyer, P. Rayson, C. Pohl, and A. Rummler. An exploratory study of information retrieval techniques in domain analysis. In Software Product Lines, 12th International Conference, SPLC 2008, pages 67–76, 2008. doi: 10.1109/SPLC.2008.18.

[3] D. Batory. Feature models, grammars, and propositional formulas. In Software Product Lines, 9th International Conference, SPLC 2005, pages 7–20. Springer Berlin Heidelberg, 2005. doi:10.1007/11554844_3.

[4] D. Benavides, S. Segura, and A. Ruiz-Cortés. Automated analysis of feature models 20 years later: A literature review. Information Systems, 35(6):615–636, 2010. doi:10.1016/j.is.2010.01.001.

[5] A. Bolotov and M. Fisher. A resolution method for CTL branching-time temporal logic. In 4th International Workshop on Temporal Representation and Reasoning, TIME ’97, pages 20–27. IEEE Computer Society, 1997. doi:10.1109/TIME.1997.600777.

[6] M. C. Browne, E/ M. Clarke, and O. Grümberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1-2):115–131, 1988. doi:10.1016/0304-3975(88)90098-9.

[7] D. Bustan and O. Grumberg. Simulation-based minimization. ACM Transactions on Computational Logic (TOCL), 4(2):181–206, 2003. doi: 10.1145/635499.635502.

[8] A. Classen, M. Cordy, P. Heymans, A. Legay, and P. Schobbens. Formal semantics, modular specification, and symbolic verification of product- line behaviour. Science of Computer Programming, 80:416–439, 2014. doi:10.1016/j.scico.2013.09.019.

[9] A. Classen, A. Hubaux, and P. Heymans. A formal semantics for multi-level staged configuration. In Third International Workshop on Variability Modelling of Software-Intensive Systems VaMoS’09, pages 51–60, 2009.

[10] M. Cordy, P. Heymans, A. Legay, P-Y. Schobbens, B. Dawagne, and M. Leucker. Counterexample guided abstraction refinement of product- line behavioural models. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 190–201, 2014. doi:10.1145/2635868.2635919.

[11] K. Czarnecki, S. Helsen, and U. Eisenecker. Staged configuration using feature models. In Software Product Lines, Third International Conference, SPLC 2004, pages 266–283. Springer, 2004. doi:10.1007/ 978-3-540-28630-1_17.

[12] K. Czarnecki, S. Helsen, and U. Eisenecker. Formalizing cardinality- based feature models and their specialization. Software Process: Improvement and Practice, 10(1):7–29, 2005. doi:10.1002/spip.213.

[13] K. Czarnecki, S. Helsen, and U. Eisenecker. Staged configuration through specialization and multilevel configuration of feature models. Software Process: Improvement and Practice, 10(2):143–169, 2005. doi: 10.1002/spip.225.

[14] K. Czarnecki and A. Wasowski. Feature diagrams and logics: There and back again. In Software Product Lines, 11th International Conference, SPLC 2007, pages 23–34. IEEE Computer Society, 2007. doi:10.1109/ SPLINE.2007.24.

[15] M. de Jonge and J. Visser. Grammars as feature diagrams. In Workshop on Generative Programming 2002 (GP’02), pages 23–24, 2002.

[16] Z. Diskin, A. Safilian, T. Maibaum, and S. Ben-David. Modeling product lines with Kripke structures and modal logic. In Theoretical Aspects of Computing – ICTAC 2015 – 12th International Colloquium, pages 184–202. Springer, 2015. doi:10.1007/978-3-319-25150-9_12.

[17] E A. Emerson and J Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Computer and System Science, 30(1):1–24, 1988. doi:10.1016/0022-0000(85)90001-7.

[18] O. Friedmann and M. Lange. A solver for modal fixpoint logics. Electronic Notes in Theoretical Computer Science, 262:99–111, 2010. doi:10.1016/j.entcs.2010.04.008.

[19] R. Gheyi, T. Massoni, and P. Borba. Automatically checking feature model refactorings. Journal of Universal Computer Science, 17(5):684– 711, 2011. doi:10.3217/jucs-017-05-0684.

[20] V. Gupta and V. R. Pratt. Gages accept concurrent behavior. In FOCS’93, pages 62–71. IEEE, 1993. doi:10.1109/SFCS.1993.366881.

[21] T. Hildebrandt and R. Mukkamala. Declarative event-based workflow as distributed dynamic condition response graphs. arXiv preprint arXiv:1110.4161, 2011. doi:10.4204/EPTCS.69.5.

[22] P. Höfner, R. Khédri, and B. Möller. An algebra of product families. Software and System Modeling, 10(2):161–182, 2011. doi:10.1007/ s10270-009-0127-2.

[23] A. Hubaux, A. Classen, and P. Heymans. Formal modelling of feature configuration workflows. In Software Product Lines, 13th International Conference, SPLC 2009, pages 221–230. Carnegie Mellon University, 2009. doi:10.1145/1753235.1753266.

[24] K C. Kang, S G. Cohen, J A. Hess, W E. Novak, and A S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical report, DTIC Document, 1990. URL: http://www.sei.cmu.edu/ reports/90tr021.pdf.

[25] M. Lange and C. Stirling. Focus games for satisfiability and completeness of temporal logic. In 16th Annual IEEE Symposium on Logic in Computer Science (LICS’01), pages 357–365. IEEE, 2001. doi:10.1109/LICS.2001.932511.

[26] M. Leucker and D. Thoma. A formal approach to software product families. In Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change – 5th International Symposium (ISoLA’12), pages 131–145. Springer, 2012. doi:10.1007/ 978-3-642-34026-0_11.

[27] M. Mannion. Using first-order logic for product line model validation. In Software Product Lines, Second International Conference (SPLC’02), pages 176–187. Springer, 2002. doi:10.1007/3-540-45652-X_11.

[28] W. Marrero. Using BDDs to decide CTL. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, pages 222–236. Springer, 2005. doi:10.1007/978-3-540-31980-1_15.

[29] M. Mendonca, A. Wasowski, K. Czarnecki, and D. Cowan. Efficient compilation techniques for large scale feature models. In Generative Programming and Component Engineering, 7th International Conference, GPCE 2008, pages 13–22. ACM, 2008. doi:10.1145/1449913.1449918.

[30] N. Niu and S. Easterbrook. On-demand cluster analysis for product line functional requirements. In Software Product Lines, 12th International Conference, SPLC 2008, pages 87–96. IEEE, 2008. doi:10.1109/SPLC.2008.11.

[31] G. Michele Pinna and Axel Poigné. On the nature of events: Another perspective in concurrency. Theoretical Computer Science, 138(2):425– 454, 1995. doi:10.1016/0304-3975(94)00174-H

[32] K. Pohl, G. Böckle, and F. Van Der Linden. Software product line engineering: foundations, principles, and techniques. Springer, 2005.

[33] V. R. Pratt. Event spaces and their linear logic. In Algebraic Methodology and Software Technology (AMAST’91), pages 3–25, 1991.

[34] A. Safilian and T. Maibaum. Hierarchical multiset theories of cardinality- based feature diagrams. In 10th International Symposium on Theoretical Aspects of Software Engineering (TASE’16), pages 136–143. IEEE, 2016. doi:10.1109/TASE.2016.14.

[35] A. Safilian, T. Maibaum, and Z. Diskin. The semantics of cardinality- based feature models via formal languages. In FM’15: Formal Methods – 20th International Symposium, pages 453–469. Springer, 2015. doi: 10.1007/978-3-319-19249-9_28.

[36] P-Y. Schobbens, P. Heymans, and J-C. Trigaux. Feature diagrams: A survey and a formal semantics. In 14th IEEE International Conference on Requirements Engineering (RE’06), pages 139–148. IEEE, 2006. doi:10.1109/RE.2006.23.

[37] S. She, R. Lotufo, T. Berger, A. Wasowski, and K. Czarnecki. Reverse engineering feature models. In Proceedings of the 33rd International Conference on Software Engineering (ICSE’11), pages 461–470. IEEE, 2011. doi:10.1145/1985793.1985856.

[38] T. Thum, D. Batory, and C. Kastner. Reasoning about edits to feature models. In 31st International Conference on Software Engineering (ICSE’09), pages 254–264. IEEE, 2009. doi:10.1109/ICSE.2009. 5070526.

[39] P. Trinidad and A R. Cortés. Abductive reasoning and automated analysis of feature models: How are they connected?. In Third Interna- tional Workshop on Variability Modelling of Software-Intensive Systems (VaMoS’09), pages 145–153, 2009.

[40] Rob J. van Glabbeek and Gordon D. Plotkin. Configuration structures. In 10th Annual IEEE Symposium on Logic in Computer Science (LICS’95), pages 199–209, 1995. doi:10.1109/LICS.1995.523257.

[41] G. Winskel. Event structure semantics for CCS and related languages, pages 561–576. Springer Berlin Heidelberg, 1982. doi:10.1007/BFb0012800.

[42] L. Zhang, U. Hustadt, and C. Dixon. A refined resolution calculus for CTL. In Automated Deduction–CADE-22, pages 245–260. Springer, 2009. doi:10.1007/978-3-642-02959-2_20.

Bibtex

@article{sacscuza:diskin2016fmoplwksaml,
  title={Faithful Modeling of Product Lines with Kripke Structures and Modal Logic},
  author={Z. Diskin and A. Safilian and T. Maibaum and S. Ben-David},
  journal={Scientific Annals of Computer Science},
  volume={26},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2016},
  pages={69--122},
  doi={10.7561/SACS.2016.1.69},
  publisher={``A.I. Cuza'' University Press}
}