D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, Learning operational requirements from goal models, 2009 IEEE 31st International Conference on Software Engineering, pp.265-275, 2009.
DOI : 10.1109/ICSE.2009.5070527

P. Asirelli, M. H. Ter-beek, S. Gnesi, and A. Fantechi, Deontic logics for modeling behavioural variability, VaMoS'09, pp.71-76, 2009.

F. Bachmann, M. Goedicke, J. C. Do-prado-leite, R. L. Nord, K. Pohl et al., A Meta-model for Representing Variability in Product Family Development, Int. Workshop on Product Family Engineering (PPE), pp.66-80, 2003.
DOI : 10.1007/978-3-540-24667-1_6

C. Baier and J. Katoen, Principles of Model Checking, 2007.

M. Calder, M. Kolberg, E. H. Magill, and S. Reiff-marganiec, Feature interaction: a critical review and considered forecast, Computer Networks, vol.41, issue.1, pp.115-141, 2003.
DOI : 10.1016/S1389-1286(02)00352-3

E. Clarke, O. Grumberg, and D. Peled, Model Checking, 1999.

A. Classen, Modelling with FTS: a collection of illustrative examples

A. Classen, P. Heymans, and P. Schobbens, What???s in a Feature: A Requirements Engineering Perspective, FASE'08, Held as Part of ETAPS'08, pp.16-30, 2008.
DOI : 10.1007/978-3-540-78743-3_2

A. Classen, P. Heymans, T. T. Tun, and B. Nuseibeh, Towards safer composition, 2009 31st International Conference on Software Engineering, Companion Volume, pp.227-230, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5070988
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.669.9006

P. C. Clements and L. Northrop, Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, 2001.

C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, vol.64, issue.12, pp.275-288, 1992.
DOI : 10.1007/BF00121128

K. Czarnecki and M. Antkiewicz, Mapping Features to Models: A Template Approach Based on Superimposed Variants, GPCE'05, pp.422-437, 2005.
DOI : 10.1007/11561347_28

K. Czarnecki and K. Pietroszek, Verifying featurebased model templates against well-formedness OCL constraints, GPCE '06, pp.211-220, 2006.

C. Ebert and C. Jones, Embedded Software: Facts, Figures, and Future, Computer, vol.42, issue.4, pp.42-52, 2009.
DOI : 10.1109/MC.2009.118

E. A. Emerson and C. S. Jutla, Tree automata, mu-calculus and determinacy (extended abstract), FOCS 32, pp.368-377, 1991.

A. Fantechi and S. Gnesi, A behavioural model for product families, ESEC-FSE'07, Companion, pp.521-524, 2007.

A. Fantechi and S. Gnesi, Formal Modeling for Product Families Engineering, 2008 12th International Software Product Line Conference, pp.193-202, 2008.
DOI : 10.1109/SPLC.2008.45

D. Fischbein, S. Uchitel, and V. Braberman, A foundation for behavioural conformance in software product line architectures, Proceedings of the ISSTA 2006 workshop on Role of software architecture for testing and analysis , ROSATEA '06, pp.39-48, 2006.
DOI : 10.1145/1147249.1147254

P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, CAV 2001, number 2102 in LNCS, pp.53-65, 2001.

A. Gruler, M. Leucker, and K. Scheidemann, Modeling and Model Checking Software Product Lines, IFIP WG 6.1 FMOODS '08, pp.113-131, 2008.
DOI : 10.1007/978-3-540-68863-1_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.5754

K. Kang, S. Cohen, J. Hess, W. Novak, and S. Peterson, Feature-oriented domain analysis (FODA) feasibility study, 1990.

J. Kramer, J. Magee, M. Sloman, and A. Lister, CONIC: an integrated approach to distributed computer control systems, IEE Proceedings E Computers and Digital Techniques, vol.130, issue.1, pp.1-10, 1983.
DOI : 10.1049/ip-e.1983.0001

K. G. Larsen, U. Nyman, and A. Wasowski, Modal I/O Automata for Interface and Product Line Theories, ESOP, pp.64-79, 2007.
DOI : 10.1007/978-3-540-71316-6_6

K. Lauenroth, S. Töhning, and K. Pohl, Model Checking of Domain Artifacts in Product Line Engineering, 2009 IEEE/ACM International Conference on Automated Software Engineering, 2009.
DOI : 10.1109/ASE.2009.16

H. C. Li, S. Krishnamurthi, and K. Fisler, Verifying cross-cutting features as open systems, SIGSOFT FSE, pp.89-98, 2002.

J. Liu, J. Dehlinger, and R. Lutz, Safety analysis of software product lines using state-based modeling, Journal of Systems and Software, vol.80, issue.11, pp.1879-1892, 2007.
DOI : 10.1016/j.jss.2007.01.047

M. Mendonca, A. Wasowski, and K. Czarnecki, SAT-based analysis of feature models is easy, SPLC'09, pp.231-240, 2009.

B. Morin, O. Barais, G. Nain, and J. Jézéquel, Taming Dynamically Adaptive Systems using models and aspects, 2009 IEEE 31st International Conference on Software Engineering, pp.122-132, 2009.
DOI : 10.1109/ICSE.2009.5070514
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.780

M. Plath and M. Ryan, Feature integration using a feature construct, Science of Computer Programming, vol.41, issue.1, pp.53-84, 2001.
DOI : 10.1016/S0167-6423(00)00018-6

P. Schnoebelen, The complexity of temporal logic model checking, Advances in Modal Logic 4, pp.393-436, 2002.

P. Schobbens, P. Heymans, J. Trigaux, and Y. Bontemps, Feature Diagrams: A Survey and a Formal Semantics, 14th IEEE International Requirements Engineering Conference (RE'06), pp.139-148, 2006.
DOI : 10.1109/RE.2006.23

W. M. Van-der-aalst, M. Dumas, F. Gottschalk, A. H. Ter-hofstede, M. L. Rosa et al., Correctness-preserving configuration of business process models, FASE'08, Held as Part of ETAPS'08, pp.46-61, 2008.

M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, LICS'86, pp.332-344, 1986.

T. Ziadi, L. Hélouët, and J. Jézéquel, Towards a UML Profile for Software Product Lines, Int. Workshop on Product Family Engineering (PPE), pp.129-139, 2003.
DOI : 10.1007/978-3-540-24667-1_10
URL : https://hal.archives-ouvertes.fr/hal-00794817