Index: /reasoner/reasoner.bib =================================================================== --- /reasoner/reasoner.bib (revision 121) +++ /reasoner/reasoner.bib (revision 122) @@ -266,4 +266,72 @@ } +@inproceedings{MendoncaWasowskiCzarnecki09, + author = {Mendonca, Marcilio and Wasowski, Andrzej and Czarnecki, Krzysztof}, + title = {SAT-based Analysis of Feature Models is Easy}, + booktitle = {Proceedings of the 13th International Software Product Line Conference}, + series = {SPLC '09}, + year = {2009}, + location = {San Francisco, California, USA}, + pages = {231--240}, + numpages = {10}, + url = {http://dl.acm.org/citation.cfm?id=1753235.1753267}, + acmid = {1753267}, + publisher = {Carnegie Mellon University}, + address = {Pittsburgh, PA, USA}, +} + +@article{BakDiskinAntkiewicz+16, + author = {Kacper Bak and + Zinovy Diskin and + Michal Antkiewicz and + Krzysztof Czarnecki and + Andrzej Wasowski}, + title = {Clafer: unifying class and feature modeling}, + journal = {Software and System Modeling}, + volume = {15}, + number = {3}, + pages = {811--845}, + year = {2016}, + url = {https://doi.org/10.1007/s10270-014-0441-1}, + doi = {10.1007/s10270-014-0441-1}, + timestamp = {Fri, 26 May 2017 22:52:21 +0200}, + biburl = {https://dblp.org/rec/bib/journals/sosym/BakDACW16}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{BenavidesTrinidadRuiz-Cortes05, + author = {Benavides, David and Trinidad, Pablo and Ruiz-Cort{\'e}s, Antonio}, + title = {Automated Reasoning on Feature Models}, + booktitle = {Proceedings of the 17th International Conference on Advanced Information Systems Engineering}, + series = {CAiSE'05}, + year = {2005}, + isbn = {3-540-26095-1, 978-3-540-26095-0}, + location = {Porto, Portugal}, + pages = {491--503}, + numpages = {13}, + url = {http://dx.doi.org/10.1007/11431855_34}, + doi = {10.1007/11431855_34}, + acmid = {2129922}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} + +@inproceedings{MendoncaBrancoCowan09, + author = {Mendonca, Marcilio and Branco, Moises and Cowan, Donald}, + title = {S.P.L.O.T.: Software Product Lines Online Tools}, + booktitle = {Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications}, + series = {OOPSLA '09}, + year = {2009}, + isbn = {978-1-60558-768-4}, + location = {Orlando, Florida, USA}, + pages = {761--762}, + numpages = {2}, + url = {http://doi.acm.org/10.1145/1639950.1640002}, + doi = {10.1145/1639950.1640002}, + acmid = {1640002}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {automated reasoning, feature model automated analysis, feature models, interactive configuration, software product lines}, +} @Comment{jabref-meta: databaseType:bibtex;} Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 121) +++ /reasoner/reasoner.tex (revision 122) @@ -67,22 +67,24 @@ \LinesNumbered -Automatically analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language \cite{EichelbergerKroeherSchmid13}. In this document, we give an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML), a variability and configuration modeling language that contains several advanced and complex modeling concepts as well as an expressive constraint language allowing for first-order logic. We discuss the approach to reasoning for IVML, in particular, the translation of types and constraints for reasoning, the reasoning algorithm, the validation of the approach and its performance for different kinds of models. +Automatically analyzing and reasoning about interdependent configuration settings can be a difficult task, in particular if the configuration modeling approach provides complex modeling concepts or a highly expressive constraint language~\cite{EichelbergerKroeherSchmid13}. In this document, we give an overview on the current state of reasoning for the Integrated Variability Modeling Language (IVML)~\cite{IVML-LS}, a variability and configuration modeling language that contains several advanced and complex modeling concepts as well as an expressive constraint language allowing for first-order logic. We discuss the approach to reasoning for IVML, in particular, the translation of types and constraints for reasoning, the reasoning algorithm, the validation of the approach and its performance for different kinds of models. \section{Introduction} -In Product Line Engineering, a \emph{variability model} defines the options to customize a software system, while a \emph{configuration} specifies the choices made for a specific instance of the software system. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another option. Such dependencies are typically expressed using different forms of \emph{constraints}. For instantiating a software system, a configuration must be valid, i.e., all (relevant) constraints must be fulfilled. To analyze a configuration for validity, for figuring out the number of remaining configuration options or for propagating derivable values, various forms of \emph{reasoning mechanisms} are utilized. Several reasoning mechanisms are available, such as SAT-solving or SMT-reasoners \TBD{cites}. However, expressiveness of the modeling concepts and supported constraints affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, also the applicable reasoning mechanism. - -Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches to textual variability modeling have been proposed~\cite{EichelbergerSchmid15a}. Moreover, there seems to be a trend that more recent variability modeling support more powerful modeling concepts~\cite{EichelbergerSchmid15a}, which then require more powerful analysis and reasoning mechanisms. As stated above, typically these mechanisms then imply limitations of the analysis capabilities, e.g., non-Boolean decisions typically prevent determining the actual number of possible configurations (of course not the number of configuration options that remain to be configured to achieve a complete configuration). - -The \emph{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (for binding times), quantification constraints, or user-defined constraint functions. This even allows for topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. In this document, we discuss the approach and recent state of the reasoning mechanism for IVML and its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}. At its core, the reasoner focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propagation as much as possible. This allows for performing typical validation and propagation tasks. In summary, the main constributions of this document are: +In Product Line Engineering, a \emph{variability model} defines the options to customize a software system, while a \emph{configuration} specifies the choices made for a specific instance / product of the product line. Customization options can depend on each other, e.g., the choice made for an option determines, restricts or even excludes the selection for another customization option. Such dependencies are typically expressed using different forms of \emph{constraints}. For instantiating a software system, a configuration must be valid, i.e., all (relevant) constraints must be fulfilled. To analyze a configuration for validity, for figuring out the number of remaining configuration options or for propagating derivable values, various forms of \emph{reasoning mechanisms} are utilized, such as SAT-solvers in \cite{BakDiskinAntkiewicz+16, BenavidesTrinidadRuiz-Cortes05, MendoncaBrancoCowan09} or SMT-reasoners in \cite{BakDiskinAntkiewicz+16}. For some models, specific forms of reasoning were even shown to be efficient, e.g., SAT-solving on feature models \cite{MendoncaWasowskiCzarnecki09}. However, the expressiveness of the modeling concepts affect the analyzability of the model~\cite{EichelbergerKroeherSchmid13}, and, thus, limit also the feasibility of applying (existing) reasoning mechanisms. + +Besides traditional variability modeling approaches, such as feature modeling~\cite{CzarneckiHelsenEisenecker05, KangCohenHess+90} or decision modeling~\cite{CzarneckiGruenbacherRabiser+12, SchmidJohn04}, in recent time several approaches with more powerful modeling concepts have been proposed, e.g., supporting non-boolean variability, sets of variabilities or advanced types of constraints, e.g., first-order logic. One rather popular form of approaches is textual variability modeling, as analyzed in more details in~\cite{EichelbergerSchmid15a}. Such more powerful modeling approaches require also adequate reasoning mechanisms, while the expressiveness of modeling concepts trades off with analyzability~\cite{EichelbergerKroeherSchmid13}. For short, typically more powerful modeling concepts imply limitations of the analysis capabilities, e.g., non-Boolean configuration options typically prevent determining the actual number of possible configurations (in contrast to the number of configuration options that remain to be configured to achieve a complete configuration). + +The \emph{Integrated Variability Modeling Language (IVML)}~\cite{IVML-LS} is a textual variability modeling language providing rather powerful modeling concepts, among them a type system inspired by object-orientation, multiple-inheritance, container types, configuration references, imports, orthogonal annotations (e.g., for binding times), quantification constraints, or user-defined constraint functions. The core idea of IVML is to represent a variability, i.e., a configuration option, as a typed variable. IVML even allows for modeling topological variability, i.e., configuring and reasoning over graph structures~\cite{EichelbergerQinSizonenko+16}. + +In this document, we discuss the approach and the design of the reasoning mechanism for IVML as well as its realization in EASy-Producer~\cite{EichelbergerEl-SharkawyKroeher+14, El-SharkawyKroeherEichelbergerSchmid15}, an Open Source product line toolset implementing IVML. At its core, the reasoner focuses on translating / creating specifically instantiated constraints for the various IVML concepts and on forward-reasoning, i.e., evaluating the constraints and performing value propagation as much as possible. On the one hand side, this allows for performing typical validation and propagation tasks, but, on the other hand side, this currently does not support advanced reasoning functionality such as configuration completion. This document is mainly intended to summarize the actual state, the ideas behind individual steps of the reasoning process and the decisions made for realizing the reasoning. Besides the pure technical documentation, our specific constributions are: \begin{itemize} \item An IVML-complete reasoning mechanism, i.e., translation and reasoning for a complex, rich and typed variability modeling language. - \item Support for IVML type refinements, i.e., types and polymorphism as known from object-orientation. IVML allows introducing a type hierarchy within a (meta-)model, and so the potential types for a variable can change along the type hierarchy. As types can introduce constraints, the actual constraint set during reasoning may change, i.e., constraints may be added or removed as an effect of a value change. - \item Support for IVML constraint variables, i.e., variables that hold constraints (including sets or sequences) and also can change during reasoning. Likewise, this must be reflected correctly by adjusting the constraint set at runtime. + \item Support for IVML type refinements, which can cause implicit effects on the application of constraints. IVML allows defining a type hierarchy, and so the potential types for a configuration option, i.e., a typed variable, can change along the type hierarchy. As types can introduce constraints, the actual constraint set considered during reasoning can change, i.e., constraints must be added or removed as an effect of a value type change. + \item Support for IVML constraint variables, i.e., variables that hold constraints (including sets or sequences) and be changed by the configuration. Through constraint variables, IVML explicitly allows introducing, adding, removing and disabling constraints. Consequently, such changes can affect the constraint set considered during reasoning. \item Instantiation of type-based constraints to variable-based constraints as a basis for a subsequent reasoning chain. For such subsequent reasoners, the IVML reasoner provides a solid basis, detailed error messages including the failed instantiated constraints so that a chained reasoner can directly continue with these constraints. We envision for future work, that further reasoning steps may add complementing reasoning functionalities such as identifying a value from narrowing constraints. \end{itemize} -This document is structured as follows: Section \ref{sectApproach} introduces the overall approach to reasoning for IVML. Section \ref{sectNotation} introduces the notation that we use to describe the reasoning algorithm, in particular the notation to access (derived) properties of the various IVML concepts. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints, reasoning and reacting to value changes / propagation. In Section \ref{sectTranslation}, we detail the instantiation and translation of constraints for individual configuration settings. The re-scheduling of constraints due to changing value types or constraints is discussed in Section \ref{sectTopLevelConstraintsRescheduling} as the respective algorithm relies on the constraint translation algoithms introduced before. In Section \ref{sectCompleteness}, we analyze the effect translations in order to assess the actual state for completeness with respect to IVML concepts. In Section \ref{sectEvaluation}, we present an evaluation of the actual evaluation with respect to performance incuding different kinds of IVML models. In Section \ref{sectPerformance}, we summarize the findings made during the revision of the reasoner with regard to performance, in particular that further modifications don't apply modify the implementation against already known performance anti-patterns. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook to future work. +This document is structured as follows: Section \ref{sectApproach} provides an overview to our approach. Section \ref{sectNotation} introduces the notation that we use throughout this document to specify the algorithms, i.e., we introduce notations for sets, sequences, substitutions as well as relevant parts of the IVML object model realizing the various IVML concepts, here in terms of notations for accessing (derived) properties of the IVML model. In Section \ref{sectReasoning}, we discuss the top-level algorithms for transforming constraints and reasoning. In Section \ref{sectTranslation}, we detail the translation of constraints for all IVML modeling concepts. The result is a set of instantiated constraints that can be used for reasoning. Section \ref{sectTranslation} includes also the mechanism for re-scheduling constraints when value types or constraint variables change, as this mechanism heavily relies on the constraint translations discussed before. In Section \ref{sectCompleteness}, we analyze the translations in order to assess their completeness with respect to IVML concepts and indicate the state of the validiation, i.e., regression test cases checking that the constraint translations are applied correctly for specific modeling situations. In Section \ref{sectEvaluation}, we present an evaluation of the actual performance of the reasoning approach for different kinds of IVML models. In Section \ref{sectPerformance}, we summarize performance issues, findings and resolutions we made while revising the reasoner, in particular to avoid that future modifications violate already resolved performance anti-patterns. Finally, in Section \ref{sectConclusion} we conclude and provide an outlook on future work. %-----------------------------------------------------------------------------------------------------------------