Index: /reasoner/reasoner.bib =================================================================== --- /reasoner/reasoner.bib (revision 122) +++ /reasoner/reasoner.bib (revision 123) @@ -33,4 +33,11 @@ booktitle = "Eclipse Technology eXchange Workshop", year = 2015 +} + +@misc{OCL24, + author = {OMG}, + title = {Object Constraint Language Specification, Version 2.4}, + year = {2014}, + url = {http://www.omg.org/spec/OCL/2.4/} } @@ -84,4 +91,66 @@ year = {2016}, pages = {204--208} +} + +@inproceedings {EichelbergerQinSchmid17a, +author={H. Eichelberger and C. Qin and K. Schmid}, +title={{Experiences with the Model-based Generation of Big Data Applications}}, +booktitle={Big Data Mgt. Systems in Business and Industrial Applications (BigBia '17)}, +year={2017}, +pages={49-56}, +abstract={Developing Big Data applications implies a lot of schematic or complex structural tasks, which can easily lead to implementation errors and incorrect analysis results. In this paper, we present a model-based approach that supports the automatic generation of code to handle these repetitive tasks, enabling data engineers to focus on the functional aspects without being distracted by technical issues. In order to identify a solution, we analyzed different Big Data stream-processing frameworks, extracted a common graph-based model for Big Data streaming applications and developed a tool to graphically design and generate such applications in a model-based fashion (in this work for Apache Storm). Here, we discuss the concepts of the approach, the tooling and, in particular, experiences with the approach based on feedback of our partners.} +} + +@inproceedings{KolliaGlimmHorrocks11, + author = {Kollia, Ilianna and Glimm, Birte and Horrocks, Ian}, + title = {SPARQL Query Answering over OWL Ontologies}, + booktitle = {Proceedings of the 8th Extended Semantic Web Conference on The Semantic Web: Research and Applications - Volume Part I}, + series = {ESWC'11}, + year = {2011}, + isbn = {978-3-642-21033-4}, + location = {Heraklion, Crete, Greece}, + pages = {382--396}, + numpages = {15}, + url = {http://dl.acm.org/citation.cfm?id=2008892.2008925}, + acmid = {2008925}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} + +@Inproceedings{DemuthLoecherZschaler04, + title = "Structure of the Dresden OCL Toolkit", + author = "B. Demuth, S. Löcher, St. Zschaler", + booktitle = "International Fujaba Days, MDA with UML and Rule-based Object Manipulation", + year = 2004 +} + +@InProceedings{ClavelEgea06, +author="Clavel, Manuel +and Egea, Marina", +editor="Johnson, Michael +and Vene, Varmo", +title="ITP/OCL: A Rewriting-Based Validation Tool for UML+OCL Static Class Diagrams", +booktitle="Algebraic Methodology and Software Technology", +year="2006", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="368--373", +abstract="In this paper we present the ITP/OCL tool, a rewriting-based tool that supports automatic validation of UML class diagrams with respect to OCL constraints. Its implementation is directly based on the equational specification of UML+OCL class diagrams. It is written entirely in Maude making extensive use of its reflective capabilities. We also give notice of the Visual ITP/OCL, a Java graphical interface that can be used as a front-end for the ITP/OCL tool.", +isbn="978-3-540-35636-3" +} + + + +@article{KahnPorres15, +title = "Consistency of UML class, object and statechart diagrams using ontology reasoners", +journal = "Journal of Visual Languages \& Computing", +volume = "26", +pages = "42 - 65", +year = "2015", +issn = "1045-926X", +doi = "https://doi.org/10.1016/j.jvlc.2014.11.006", +url = "http://www.sciencedirect.com/science/article/pii/S1045926X14001323", +author = "Ali Hanzala Khan and Ivan Porres", +keywords = "Consistency, Ontology, UML, Reasoning" } Index: /reasoner/reasoner.tex =================================================================== --- /reasoner/reasoner.tex (revision 122) +++ /reasoner/reasoner.tex (revision 123) @@ -81,6 +81,6 @@ \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, 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 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 base 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 base 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} @@ -92,21 +92,25 @@ \section{Approach}\label{sectApproach} -IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to~\cite{IVML-LS} for the complete specification), is based on well known (programming) language concepts to express the (meta-) model of a configuration as well as individual configuration instances. The main concept of IVML is the \emph{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, allows multi-inheritance), container types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by OCL concepts (and notation), but, in contrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of projects), can be imported, staged~\cite{CzarneckiHelsenEisenecker05a} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. - -Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines~\cite{QMD42}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective mechanism and executing that mechanism on the translated model. While traditional reasoners allow for completing the model through feasible ground instances, they typically also perform a kind of constrained state space evaluation. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables), just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} lead to a significant and infeasible runtime overhead. Moreover, these both kinds of approaches are limited as they typically do not directly support the breadth of OCL operations, in particular container iterators, quantifiers and user-defined constraint operations. In contrast, specific reasoning approaches, e.g., for OWL partially support quantification, but are similarly limited. Moreover, relying on OCL reasoning mechanisms could be a feasible approach, but would require significant extension to enable value propagation and IVML-specific operations. - -Due to these experiences, we decided to realize a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis is \emph{forward-chaining}, i.e., evaluation of a given constraint set as long as no constraints are left over, while re-scheduling constraints attached to a variable if the variable changes during reasoning. It is important to notice that IVML~\cite{IVML-LS} supports a declarative specification of constraints, i.e., they can be given regardless of their actual evaluation sequence. To ensure that values are uniquely determined, IVML allows changing the value of a constraint only once within a project scope, otherwise requiring that a reasoning mechanism issues an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in certain cases, some form of sequence of the constraints can be indicated through partial evaluations, i.e., eval-blocks within a project or a compound. An eval-block consists of constraints or nested eval-blocks. IVML~\cite{IVML-LS} considers project as outermost (implicit) eval-scope, then eval-blocks are evaluated in their nesting sequence (whereby eval-blocks on the same nesting level do not imply any sequence). - -However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined directly on compound types, or indirectly, through types used within collections. Specifying IVML constraints on types, such as compounds, rather than variables (where applicable) simplifies the model (for a compound such constraints are automatically valid for all instances without explicit quantification), supports consistency and helps reduces the model size and complexity. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVML{self} pointing to the actual compound instance. Cross-references to other types are required to be specified through an explicit accessor, i.e., an expression mentioning the variable and the respective nested variable(s). During reasoning, constraints over types cannot be evaluated, as the actual values are not available. Thus, we perform first a \emph{constraint translation step} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative here could be reasoning over the type constraints and modifying the mapping on demand before evaluation. This could save memory and runtime (for constraint translation / creation), but, however, increases complexity in managing the actual constraints to be evaluated. So we opted for instantiating the constraints and keeping only the new, failed or recently affected ones in the constraint base. - -Based on our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of default-value logic, project scopes, eval-block scopes), the reasoning mechanism shall directly operate on an IVML model. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. In particular no complete model transformations as we did in previous approaches to maximize reuse of existing reasoning mechanisms is infeasible. After the required constraint translation, constraint evaluation and forward-chaining is executed on this constraint base. As this approach is not reasoning complete (while through construction IVML complete), we can imagine that specific reasoning engines such as SMT could complement the described approach. Therefore, translating the failed constraints into a model that is suitable for sophisticated reasoning approaches could enable advanced capabilities, such as value determination, instance creation or configuration completion / repair. - -Typically, reasoning over all variables of a project including all constraints is needed. This may differ for initializing a model through the reasoner (assign first default values in a first round, perform a reasoning round in a second round) as well as in use cases where considering all constraints is explicitly not needed and even not efficient with respect to reasoning time. The first case is \emph{incremental reasoning}, i.e., starting with a given (valid) configuration and just analyzing the changes made by the user. The idea is to provide nearly immediate results, so that reasoning even on complex and large models can happen on every change made by the user. The second case is \emph{runtime reasoning}, e.g., reasoning for validity at runtime of a system to identify deviations and to trigger re-configuration or adaptation \cite{Eichelberger16}. For these cases, we introduce two main \emph{reasoning modes}, namely full reasoning and incremental reasoning, while the latter can be achieved through the following two techniques. +IVML is a textual variability and configuration modeling language. The syntax of IVML, which is mostly out of scope here (please refer to~\cite{IVML-LS} for the complete specification), is based on well known (programming) language concepts and can be used to express the (meta-)model of a configuration as well as individual configurations. The main concept of IVML is the \emph{typed variable}, which may have a default value expression. For short, IVML offers basic types (Boolean, Integer, Real, String), user-defined compound types (groups of variables, can be subject to multi-inheritance), container types (set, sequence), derived types (constraining or aliasing another type) and constraint types, i.e. variables holding a constraint so that it can be overridden by assigning a new constraint. IVML variables can be further detailed by and interrelated with other variables through constraints. The constraint (expression) language is largely inspired by concepts (and notation) of the Object Constraint Language (OCL)~\cite{OCL24}, but, in contrast to OCL, allows side-effect to enable the definition of configurations as well as the propagation of configuration values. IVML models (given in terms of so called \IVML{projects}), can be imported, staged~\cite{CzarneckiHelsenEisenecker05a} and conditionally frozen, in particular to enable partial instantiation of code, including removal of variation points. + +Over the last years, we approached the analysis and reasoning for IVML from different perspectives, including traditional reasoning mechanisms or rule engines~\cite{QMD42}. Although these mechanisms are powerful in their own respect and typically available as implementation, using them for IVML requires translating an IVML model and its constraints into the model of the respective reasoning mechanism and executing that mechanism on the translated model. In the past, we identified in particular this transformation as performance bottleneck as well as an obstacle to achieve IVML-completeness, i.e., we were often not able to express all IVML concepts in the respective reasoner model. While traditional reasoners allow for completing a model through feasible ground instances, they typically also perform a kind of constrained state space exploration. Considering the size of usual configuration models (currently the largest IVML model we are aware of has more than 16.000 variables \cite{EichelbergerQinSizonenko+16, EichelbergerQinSchmid17a}), we experienced that just applying a traditional reasoner to usual IVML models is an inefficient approach. Other related mechanisms such as rule engines can be applied to some degree, however, according to our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} lead to a significant and infeasible runtime overhead. Moreover, traditional reasoners as well as rule engines are limited as they typically do not support the range of OCL operations required for IVML, in particular container iterators, quantifiers and user-defined constraint operations. Further, also specific reasoning approaches, e.g., for the Object Web Language (OWL) \cite{KahnPorres15, KolliaGlimmHorrocks11} might be an option as they partially support quantification, but they are similarly limited regarding the range of OCL operations. Moreover, OCL-based approaches such as \cite{DemuthLoecherZschaler04, ClavelEgea06} typically also focus on forward-chaining, but would require deep extensions, as OCL does not allow for side-effects or value propagation as required by IVML. + +Due to these experiences, we decided to pursue a \emph{mixed reasoning approach}, which attempts to reduce / simplify the reasoning problem towards an instance that (if needed) can finally be handled by a traditional reasoning approach. The basis for this mixed approach is \emph{forward-chaining}, i.e., evaluation of a given constraint base as long as no constraints are left over, while re-scheduling constraints that depend on a variable changed during reasoning. The SSE IVML reasoner as described in this document realizes this basis, while the actual mixed approach is part of future work. + +It is important to notice that IVML~\cite{IVML-LS} supports declarative specification of constraints, i.e., modeling concepts and constraints can be specified regardless of their actual evaluation sequence. To ensure that values for variables are uniquely determined, in particular in presence of default values, IVML allows changing the value of a variable only once within a project scope. Otherwise the reasoning mechanism must issue an error. Thus, reasoning must happen project-wise, in a depth-first traversal along the project import dependencies. Moreover, to speed up reasoning in specific situations, some form of sequence of the constraints can be indicated through the concept of partial evaluations, i.e., eval-blocks stated within a project or a compound. An eval-block consists of constraints or nested eval-blocks, while nested eval-blocks implicitly define an evaluation sequence. In other words, a project is the outermost (implicit) eval-block and nested eval-blocks shall be evaluated in their nesting sequence, while eval-blocks on the same nesting level do not imply any evaluation sequence. + +However, not all IVML constraints can be directly used for reasoning. This is in particular true for constraints defined in compound types, i.e., these constraints must hold for all instances, or, indirectly, through types used within collections, i.e., these constraints must hold for the respective collection elements. Such constraints typically utilize local variables defined within the compound including the special pre-defined variable \IVML{self} pointing to the actual compound instance. Allowing such implicit constraints rather than requiring that all constraints are defined directly on the configuration variables increases consistency and helps reducing model sizes and complexity. +%Cross-references to other types are required to be specified through an explicit accessor, i.e., an expression mentioning the variable and the respective nested variable(s). +As a consequence, the reasoning mechanism must relate type-based constraints to the correct underlying configuration variables. In our approach, we perform first a \emph{constraint translation} to instantiate the constraints for configuration variables based on the actual type of the variable or its value. An alternative could be reasoning over type constraints and modifying the mapping to the variables on demand before evaluation. This may save memory and runtime (required for constraint translation / creation), but, however, also increases the complexity of managing the actual constraints to be evaluated. + +Based on our experience \cite{EichelbergerQinSizonenko+16, QMD42, QMD43} and taking into account the specific requirements of the default values, project scopes, eval-block scopes, we are convinced that (at least the first step in a mixed reasoning approach) shall directly operate on an IVML model, also to achieve a high runtime performance. In particular, model transformations such as the constraint translation shall happen only if required to reduce overhead on the reasoning time. After the required constraint translation, constraint evaluation and forward-chaining is executed on the collected constraint base. Besides the resulting configuration, \emph{detained reasoning output} is required, so that subsequent reasoners in a reasoning chain can continue on the results. For this purpose, reasoning error messages shall not only contain the failed constraint, but also additional information such as failing sub-expressions. Based on such output, we can imagine that more advanced reasoning engines such as SMT-reasoners could complement the described approach. Translating the information about failed constraints into a model that is suitable for sophisticated reasoning approaches could enable advanced capabilities, such as value determination, instance creation or configuration completion / repair. However, such chained reasoning is out of the scope of this document. + +Basically, reasoning over all variables of a project including all constraints is needed. This may differ for certain use cases where considering all constraints neither required nor efficient in terms of reasoning time. The first use case is \emph{incremental reasoning}, i.e., starting with a given configuration and just analyzing the changes made by the user. The idea is to provide immediate reasoning results, so that reasoning even on complex and large models can happen upon every change made by the user. The second use case is \emph{runtime reasoning}, e.g., reasoning for validity of a configuration at runtime of a system to identify validations and to trigger re-configuration or adaptation \cite{Eichelberger16}. In this case, we may assume that the underlying IVML model is not changed, so that initially translated constraints can be re-used. This assumption may does not hold in the incremental reasoning case. For supporting these two cases, we introduce two main \emph{reasoning modes}, namely complete (full) reasoning and incremental reasoning, while incremental reasoning can be achieved through the following two techniques. \begin{itemize} - \item \emph{Creation of a partial constraint base:} Using this technique, certain constraint types such as default-values (\TBD{or constraints for frozen values}) are not added to the constraint base and the related variables are assumed to be properly instantiated through an initial reasoning run. Thus, reasoning focuses on the non-frozen variables, in particular changed variables. In our experiments, this mechanism can save up to 65\% reasoning time. This mode can be activated through the reasoner configuration. - \item \emph{Re-using a previously build constraint base:}. Trading off less reasoning time (\TBD{measure effect}) with memory for storing a copy of the constraint base, we require that the underlying project does not change structurally, i.e., no new types or variables are declared between two reasoning steps. This mode can be activated by requesting a re-usable reasoner instance from the EASy reasoner core and using that instance instead of the default interface (the static reasoning fronted) and it can be combined with the mechanisms for creating a partial constraint base, i.e., skipping default constraints or constraints if all dependent variables are frozen. + \item \emph{Creation of a partial constraint base:} Constraints assigning already processed default values or constraints over variables that cannot change anymore (frozen variables) are not added to the constraint base. The remaining configuration variables are assumed to be properly initialized or shall be instantiated by the reasoner if possible. Thus, reasoning focuses on non-frozen variables\footnote{In EASy-Producer, this technique can be enabled through the reasoner configuration.}, in particular changed variables. In our experiments, this mechanism can save up to 65\% reasoning time. + \item \emph{Re-using a previously created constraint base:} The initial constraint base created by the constraint translation is stored in memory and re-stored when applying the reasoner again to the same (structurally unchanged) model, i.e., we require that no new types or variables are added between two reasoning runs. This technique\footnote{This technique can be applied by requesting a re-usable reasoner instance from the EASy-Producer reasoner core and by using that instance instead of the default interface provided by the static reasoning fronted.} trades off reasoning time for memory consumption and can even be combined with creating a partial constraint base, saving up to further 75\% reasoning time. \end{itemize} -To implement the IVML reasoner, we designed and realized first an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. This includes constraint expressions (expressions evaluating to a Boolean value) and as special case default value expressions (evaluating to a value that can be assigned to the respective variable). We do not detail the constraint evaluation mechanism further here, rather than focusing on the IVML reasoning mechanism, which relies on the expression evaluation mechanism for evaluating constraints. +To implement the IVML reasoner, we first designed and realized an \emph{expression evaluation mechanism}, which is able to evaluate individual IVML expressions. The evaluation mechanisms covers constraint expressions (expressions evaluating to a Boolean value) as well as general default value expressions. The reasoner relies on that mechanism, i.e., in the algorithms described in this document, we just refer to the evaluation mechanism without further detailing it. We assume that the mechanism either returns the correctly evaluated value of an expression with respect to a given model / configuration or that it indicates that the evaluation result is undefined, e.g., as configuration variables used in the evaluated expression are undefined. %-----------------------------------------------------------------------------------------------------------------