Metamodel Instance Generation: A systematic literature review
---
paper_title: Test Sequence Generation from UML Sequence Diagrams

paper_content:

In this paper, we present an approach to generate test sequences from UML 2.0 sequence diagrams. Sequence diagrams are one of the most widely used UML models in the software industry. Although sequence diagrams are used for modeling the dynamic aspects of the system, they can also be used for model based testing. Existing work does not encompass certain important features of UML 2.0 sequence diagrams. Our work considers many of the novel features of UML 2.0 sequence diagrams like alt, loop, opt and break to generate test sequences. These areimportant features as far as testing is concerned. Our work begins with defining the important types of relationship that can exist between the messages. Based on the relationship between the messages, the message sequences are generated. Our work considers an important feature of UML 2.0 sequence diagrams called the dasiaExecution Occurrencepsila to generate message sequences. Next, an intermediate representation of the sequence diagram is built. This intermediate representation is called the Sequence Dependency Graph (SDG). The message sequences are incorporated into the SDG. Finally, we discuss a traversal algorithm to generate test sequences from SDG. Our method is fully automated and the test sequences generated can be used to check the correctness of the implementation under test.
---
paper_title: Model-based test cases synthesis using UML interaction diagrams

paper_content:

UML 2.0 interaction diagrams model interactions in complex systems by means of operation fragments and a systematic testing approach is required for the identification and selection of test cases. The major problem for test cases synthesis from such an interaction diagram is to arrive at a comprehensive system behavior in the presence of multiple, nested fragments. In this regard, our approach is towards systematic interpretation of flow of controls as well as their subsequent usage in the test case synthesis. We also simplify the proposed flow of controls on the basis of control primitives resulting from UML 2.0 fragments and bring it to a testable form known as intermediate testable model (ITM), which is suitable for deriving system level test cases.
---
paper_title: Regression testing with UML software designs: A survey

paper_content:

The unified modeling language (UML) designs come in a variety of different notations. UML designs can be quite large and interactions between various notations and the models they define can be difficult to assess. During the design phase, and between successive releases of systems, designs change. The impact of such changes and the resulting effect on behavior can be non-obvious and difficult to assess. This survey article explores techniques for such re-evaluation that can be classified as regression testing and suggests regression testing criteria for designs. These might vary depending on testing objectives and include both selective and regenerative regression testing approaches. The article provides a concise overview of regression testing approaches related to various UML design notations including use cases, class diagrams, sequence diagrams, activity diagrams, and statecharts, as well as combinations of these models. It discusses UML-related techniques involving cost and prioritization during selective regression testing. Finally, it evaluates these techniques with respect to inclusiveness, precision, efficiency, generality, accountability, and safety. An example is used throughout to illustrate how the techniques work. Copyright © 2009 John Wiley & Sons, Ltd. ::: ::: This survey article explores techniques for regression testing with UML designs and suggests regression testing criteria for designs. These might vary depending on testing objectives and include both selective and regenerative regression testing approaches. The article provides a concise overview of regression testing approaches related to various UML design notations including use cases, class diagrams, sequence diagrams, activity diagrams, and statecharts, as well as combinations of these models. Copyright © 2009 John Wiley & Sons, Ltd.
---
paper_title: Closing the gap between modelling and java

paper_content:

Model-Driven Software Development is based on standardised models that are refined, transformed and eventually translated into executable code using code generators. However, creating plain text from well-structured models creates a gap that implies several drawbacks: Developers cannot continue to use their model-based tool machinery, relations between model elements and code fragments are hard to track and there is no easy way to rebuild models from their respective code. ::: ::: This paper presents an approach to bridge this gap for the Java programming language. It defines a full metamodel and text syntax specification for Java, from which a parser and a printer are generated. Through this, Java code can be handled like any other model. The implementation is validated with large test sets, example applications are shown, and future directions of research are discussed.
---
paper_title: Compiler test case generation methods: a survey and assessment

paper_content:

Abstract Software testing is an important and critical phase of the application software development life cycle. Testing is a time consuming and costly stage that requires a high degree of ingenuity. In the development stages of safety-critical and dependable computer software such as language compilers and real-time embedded software, testing activities consume about 50% of the project time. In this work we address the area of compiler testing. The aim of compiler testing is to verify that the compiler implementation conforms to its specifications, which is to generate an object code that faithfully corresponds to the language semantic and syntax as specified in the language documentation. A compiler should be carefully verified before its release, since it has to be used by many users. Finding an optimal and complete test suite that can be used in the testing process is often an exhaustive task. Various methods have been proposed for the generation of compiler test cases. Many papers have been published on testing compilers, most of which address classical programming languages. In this paper, we assess and compare various compiler testing techniques with respect to some selected criteria and also propose some new research directions in compiler testing of modem programming languages.
---
paper_title: The object constraint language: precise modeling with UML

paper_content:

(All chapters conclude with "Summary".) Foreword. Preface. Acknowledgments. Introduction. Who Should Read This Book. How This Book Should Be Used. Typeface Conventions. Information on Related Subjects. 1. Why Write Constraints? Definition of Constraint. Use of Constraints in Other Techniques. Design by Contract. Definition of Contract. Contents of a Contract. Advantages of Contracts. Preconditions and Postconditions. Invariants. Advantages of Constraints. Better Documentation. Improved Precision. Communication without Misunderstanding. Declarative or Operational Constraints. Advantages of a Declarative Language. Notation: Natural Language or Mathematical Expressions. Summary: Requirements for OCL. 2. OCL Basics. The "Royal and Loyal" System Example. Putting Invariants on Attributes. Putting Invariants on Associated Classes. Dealing with Collections of Objects. Sets, Bags, and Sequences. Inheritance. Working with Enumerations. Writing Preconditions and Postconditions. Where to Start Writing Invariants. Broken Constraints. Summary. 3. The Complete Overview of OCL Constructs. Types and Instances. Value Types and Object Types. OCL Expressions and OCL Constraints. The Context of an OCL Expression. The Context of an Invariant. The Context of a Pre- or Postcondition. The self Keyword. Basic Types and Operators. The Boolean Type. The Integer and Real Types. The String Type. Model Types. Attributes from the UML Model. Operations from the UML Model. Class Operations and Attributes from the UML Model. Associations and Aggregations from the UML Model. Association Classes from the UML Model. Qualified Associations from the UML Model. Using Package Names in Navigations. Using Pathnames in Inheritance Relations. Enumeration Types. The Set, Bag, and Sequence Types. Treating Instances as Collections. Flattening Collections. Operations on All Collection Types. Operations with Variant Meaning. Operations for the Set Type. Operations for the Sequence Type. Operations That Iterate over Collection Elements. The select Operation. The reject Operation. The collect Operation. Shorthand Notation for collect. The forAll Operation. The exists Operation. The iterate Operation. Constructs for Postconditions. Operations Defined on Every OCL Type. Types as Objects. Type Conformance Rules. Precedence Rules. Comments. Undefined. Summary. 4. Modeling with Constraints. Constraints in a UML Model. Invariants. Invariants for Derived Attributes or Associations. Preconditions and Postconditions. Guards in State Transition Diagrams. Using Guards and Events in Pre- and Postconditions. Change Events in State Transition Diagrams. Type Invariants for Stereotypes. Where OCL Expressions Can Be Used. Constraints and Inheritance. Styles for Specifying Constraints. Avoiding Complex Navigation Expressions. Choice of Context Object. Use of allInstances. Splitting and Constraints. Adding Extra Operations or Attributes. Using the collect Shorthand. Solving Modeling Issues with Constraints. Abstract Classes. Specifying Uniqueness Constraints. Adding Details to the Model versus Adding Constraints. Cycles in Class Models. Constraints on Associations. Multiplicity Constraints. The Subset Constraint. The Or Constraint. Optional Multiplicity in Associations. Summary. 5. Extending OCL. A Word of Caution. Extending the Standard OCL Types. Adding New OCL Types. Operational Use of Constraints. Generating Code for Constraints. When to Check Constraints. What to Do When the Constraint Fails. Summary. Appendix A. OCL Basic Types and Collection Types. Basic Types. OclType. OclAny. OclExpression. Real. Integer. String. Boolean. Enumeration. Collection-Related Types. Collection. Set. Bag. Sequence. Appendix B. Formal Grammar. Bibliography. Index. 0201379406T04062001
---
paper_title: The category-partition method for specifying and generating fuctional tests

paper_content:

An apparatus for recovering pulse-code modulated digital data from a readback signal has equipment for partially equalizing the readback signal, and equipment for completing the partial equalization of the readback signal and for detecting the digital data. The latter equipment includes a delay device for delaying the partially equalized readback signal, equipment for providing a relatively undelayed version of the readback signal, and a differential amplifier for providing a digital signal corresponding to the difference between the delayed readback signal and the relatively undelayed version of the readback signal. The delay device includes a filter for completing the above mentioned partial equalization with the aid of the equipment for providing the relatively undelayed version of the readback signal and the mentioned differential amplifier.
---
paper_title: Validation of Model Transformations - First Experiences Using a White Box Approach

paper_content:

Validation of model transformations is important for ensuring their quality. Successful validation must take into account the characteristics of model transformations and develop a suitable fault model on which test case generation can be based. In this paper, we report our experiences in validating a number of model transformations and propose three techniques that can be used for constructing test cases.
---
paper_title: Metamodel-based Test Generation for Model Transformations: an Algorithm and a Tool

paper_content:

In a Model-Driven Development context (MDE), model transformations allow memorizing and reusing design know-how, and thus automate parts of the design and refinement steps of a software development process. A model transformation program is a specific program, in the sense it manipulates models as main parameters. Each model must be an instance of a "metamodel", a metamodel being the specification of a set of models. Programming a model transformation is a difficult and error-prone task, since the manipulated data are clearly complex. In this paper, we focus on generating input test data (called test models) for model transformations. We present an algorithm to automatically build test models from a metamodel.
---
paper_title: Automatic test case optimization using a bacteriological adaptation model: application to .NET components

paper_content:

In this paper, we present several complementary computational intelligence techniques that we explored in the field of .Net component testing. Mutation testing serves as the common backbone for applying classical and new artificial intelligence (AI) algorithms. With mutation tools, we know how to estimate the revealing power of test cases. With AI, we aim at automatically improving test case efficiency. We therefore looked first at genetic algorithms (GA) to solve the problem of test. The aim of the selection process is to generate test cases able to kill as many mutants as possible. We then propose a new AI algorithm that fits better to the test optimization problem, called bacteriological algorithm (BA): BAs behave better that GAs for this problem. However, between GAs and BAs, a family of intermediate algorithms exists: we explore the whole spectrum of these intermediate algorithms to determine whether an algorithm exists that would be more efficient than BAs.: the approaches are compared on a .Net system.
---
paper_title: Verifying UML/OCL Operation Contracts

paper_content:

In current model-driven development approaches, software models are the primary artifacts of the development process. Therefore, assessment of their correctness is a key issue to ensure the quality of the final application. Research on model consistency has focused mostly on the models' static aspects. Instead, this paper addresses the verification of their dynamic aspects, expressed as a set of operations defined by means of pre/postcondition contracts. ::: ::: This paper presents an automatic method based on Constraint Programming to verify UML models extended with OCL constraints and operation contracts. In our approach, both static and dynamic aspects are translated into a Constraint Satisfaction Problem. Then, compliance of the operations with respect to several correctness properties such as operation executability or determinism are formally verified.
---
paper_title: The Design of a Relational Engine

paper_content:

The key design challenges in the construction of a SAT-based relational engine are described, and novel techniques are proposed to address them. An efficient engine must have a mechanism for specifying partial solutions, an effective symmetry detection and breaking scheme, and an economical translation from relational to boolean logic. These desiderata are addressed with three new techniques: a symmetry detection algorithm that works in the presence of partial solutions, a sparse-matrix representation of relations, and a compact representation of boolean formulas inspired by boolean expression diagrams and reduced boolean circuits. The presented techniques have been implemented and evaluated, with promising results.
---
paper_title: Z3: An Efficient SMT Solver

paper_content:

Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.
---
paper_title: Generating Instance Models from Meta Models

paper_content:

Meta modeling is a wide-spread technique to define visual languages, with the UML being the most prominent one. Despite several advantages of meta modeling such as ease of use, the meta modeling approach has one disadvantage: It is not constructive i. e. it does not offer a direct means of generating instances of the language. This disadvantage poses a severe limitation for certain applications. For example, when developing model transformations, it is desirable to have enough valid instance models available for large-scale testing. Producing such a large set by hand is tedious. In the related problem of compiler testing, a string grammar together with a simple generation algorithm is typically used to produce words of the language automatically. In this paper, we introduce instance-generating graph grammars for creating instances of meta models, thereby overcoming the main deficit of the meta modeling approach for defining languages.
---
paper_title: Integrating meta-modelling aspects with graph transformation for efficient visual language definition and model manipulation

paper_content:

Visual languages (VLs) play a central role in modelling various system aspects. Besides standard languages like UML, a variety of domain-specific languages exist which are the more used the more tool support is available for them. Different kinds of generators have been developed which produce visual modelling environments based on VL specifications. To define a VL, declarative as well as constructive approaches are used. The meta modelling approach is a declarative one where classes of symbols and relations are defined and associated to each other. Constraints describe additional language properties. Defining a VL by a graphs grammar, the constructive way is followed where graphs describe the syntax of models and graph rules formulate the language grammar. In this paper, we extend algebraic graph grammars by a node type inheritance concept which opens up the possibility to integrate both approaches by identifying symbol classes with node types and associations with edge types of some graph class. In this way, declarative as well as constructive elements may be used for language definition and model manipulation. Two concrete approaches, the GENGED and the AToM 3 approach, illustrate how VLs can be defined and models can be manipulated by the techniques described above.
---
paper_title: On the Complexity of Derivation in Propositional Calculus

paper_content:

The question of the minimum complexity of derivation of a given formula in classical propositional calculus is considered in this article and it is proved that estimates of complexity may vary considerably among the various forms of propositional calculus. The forms of propositional calculus used in the present article are somewhat unusual, † but the results obtained for them can, in principle, be extended to the usual forms of propositional calculus.
---
paper_title: A Metamodel for the Measurement of Object-Oriented Systems: An Analysis using Alloy

paper_content:

This paper presents a MOF-compliant metamodel for calculating software metrics and demonstrates how it is used to generate a metrics tool that calculates coupling and cohesion metrics. We also describe a systematic approach to the analysis of MOF-compliant metamodels and illustrate the approach using the presented metamodel. In this approach, we express the metamodel using UML and OCL and harness existing automated tools in a framework that generates a Java implementation and an Alloy specification of the metamodel, and use this both to examine the metamodel constraints, and to generate instantiations of the metamodel. Moreover, we describe how the approach can be used to generate test data for any software based on a MOF-compliant metamodel. We extend our framework to support this approach and use it to generate a test suite for the metrics calculation tool that is based on our metamodel.
---
paper_title: Alloy: a lightweight object modelling notation

paper_content:

Alloy is a little language for describing structural properties. It offers a declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints and yet amenable to a fully automatic semantic analysis. Its meaning is given by translation to an even smaller (formally defined) kernel. This paper presents the language in its entirety, and explains its motivation, contributions and deficiencies.
---
paper_title: Verification of UML/OCL Class Diagrams using Constraint Programming

paper_content:

In the MDD and MDA approaches, models become the primary artifacts of the development process. Therefore, assessment of the correctness of such models is a key issue to ensure the quality of the final application. In that sense, this paper presents an automatic method that uses the Constraint Programming paradigm to verify UML class diagrams extended with OCL constraints. In our approach, both class diagrams and OCL constraints are translated into a Constraint Satisfaction Problem. Then, compliance of the diagram with respect to several correctness proper- ties such as weak and strong satisfiability or absence of con- straint redundancies can be formally verified.
---
paper_title: EMFtoCSP: A tool for the lightweight verification of EMF models

paper_content:

The increasing popularity of MDE results in the creation of larger models and model transformations, hence converting the specification of MDE artefacts in an error-prone task. Therefore, mechanisms to ensure quality and absence of errors in models are needed to assure the reliability of the MDE-based development process. Formal methods have proven their worth in the verification of software and hardware systems. However, the adoption of formal methods as a valid alternative to ensure model correctness is compromised for the inner complexity of the problem. To circumvent this complexity, it is common to impose limitations such as reducing the type of constructs that can appear in the model, or turning the verification process from automatic into user assisted. Since we consider these limitations to be counterproductive for the adoption of formal methods, in this paper we present EMFtoCSP, a new tool for the fully automatic, decidable and expressive verification of EMF models that uses constraint logic programming as the underlying formalism.
---
paper_title: Automatic Model Generation Strategies for Model Transformation Testing

paper_content:

Testing model transformations requires input models which are graphs of inter-connected objects that must conform to a meta-model and meta-constraints from heterogeneous sources such as well-formedness rules, transformation pre-conditions, and test strategies. Manually specifying such models is tedious since models must simultaneously conform to several meta-constraints. We propose automatic model generation via constraint satisfaction using our tool Cartier for model transformation testing. Due to the virtually infinite number of models in the input domain we compare strategies based on input domain partitioning to guide model generation. We qualify the effectiveness of these strategies by performing mutation analysis on the transformation using generated sets of models. The test sets obtained using partitioning strategies gives mutation scores of up to 87% vs. 72% in the case of unguided/random generation. These scores are based on analysis of 360 automatically generated test models for the representative transformation of UML class diagram models to RDBMS models.
---
paper_title: Translation of Restricted OCL Constraints into Graph Constraints for Generating Meta Model Instances by Graph Grammars

paper_content:

The meta modeling approach to syntax definition of visual modeling techniques has gained wide acceptance, especially by using it for the definition of UML. Since meta-modeling is non-constructive, it does not provide a systematic way to generate all possible meta model instances. In our approach, an instance-generating graph grammar is automatically created from a given meta model. This graph grammar ensures correct typing and cardinality constraints, but OCL constraints for the meta model are not supported yet. To satisfy also the given OCL constraints, well-formedness checks have to be done in addition. We present a restricted form of OCL constraints that can be translated to graph constraints which can be checked during the instance generation process.
---
paper_title: Defining Models - Meta Models versus Graph Grammars

paper_content:

The precise specification of software models is a major concern in model-driven design of object-oriented software. Metamodelling and graph grammars are apparent choices for such specifications. Metamodelling has several advantages: it is easy to use, and provides procedures that check automatically whether a model is valid or not. However, it is less suited for proving properties of models, or for generating large sets of example models. Graph grammars, in contrast, offer a natural procedure - the derivation process - for generating example models, and they support proofs because they define a graph language inductively. However, not all graph grammars that allow to specify practically relevant models are easily parseable. In this paper, we propose contextual star grammars as a graph grammar approach that allows for simple parsing and that is powerful enough for specifying non-trivial software models. This is demonstrated by defining program graphs, a language-independent model of object-oriented programs, with a focus on shape (static structure) rather than behavior.
---
paper_title: Qualifying input test data for model transformations

paper_content:

Model transformation is a core mechanism for model-driven engineering (MDE). Writing complex model transformations is error-prone, and efficient testing techniques are required as for any complex program development. Testing a model transformation is typically performed by checking the results of the transformation applied to a set of input models. While it is fairly easy to provide some input models, it is difficult to qualify the relevance of these models for testing. In this paper, we propose a set of rules and a framework to assess the quality of given input models for testing a given transformation. Furthermore, the framework identifies missing model elements in input models and assists the user in improving these models.
---
paper_title: Encoding OCL data types for SAT-based verification of UML/OCL models

paper_content:

Checking the correctness of UML/OCL models is a crucial task in the design of complex software and hardware systems. As a consequence, several approaches have been presented which address this problem. Methods based on satisfiability (SAT) solvers have been shown to be very promising in this domain. Here, the actual verification task is encoded as an equivalent bit-vector instance to be solved by an appropriate solving engine. However, while a bit-vector encoding for basic UML/OCL constructs has already been introduced, no encoding for nontrivial OCL data types and operations is available so far. In this paper, we close this gap and present a bit-vector encoding for more complex OCL data types, i.e. sets, bags, and their ordered counterparts. As a result, SAT-based UML/OCL verification becomes applicable for models containing these collections types. A case study illustrates the application of this encoding.
---
paper_title: Automating first-order relational logic

paper_content:

An automatic analysis method for first-order logic with sets and relations is described. A first-order formula is translated to a quantifier-free boolean formula, which has a model when the original formula has a model within a given scope (that is, involving no more than some finite number of atoms). Because the satisfiable formulas that occur in practice tend to have small models, a small scope usually suffices and the analysis is efficient. The paper presents a simple logic and gives a compositional translation scheme. It also reports briefly on experience using the Alloy Analyzer, a tool that implements the scheme.
---
paper_title: New Techniques that Improve MACE-style Finite Model Finding

paper_content:

We describe a new method for finding finite models of unsorted first-order logic clause sets. The method is a MACE-style method, i.e. it ”flattens” the first-order clauses, and for increasing model sizes, instantiates the resulting clauses into propositional clauses which are consecutively solved by a SAT-solver. We enhance the standard method by using 4 novel techniques: term definitions, which reduce the number of variables in flattened clauses, incremental SAT, which enables reuse of search information between consecutive model sizes, static symmetry reduction, which reduces the number of isomorphic models by adding extra constraints to the SAT problem, and sort inference, which allows the symmetry reduction to be applied at a finer grain. All techniques have been implemented in a new model finder, called Paradox, with very promising results.
---
paper_title: Grammar Testing

paper_content:

Grammar testing is discussed in the context of grammar engineering (i.e., software engineering for grammars). We propose a generalisation of the known rule coverage for grammars, that is, context-dependent branch coverage. We investigate grammar testing, especially coverage analysis, test set generation, and integration of testing and grammar transformations. Grammar recovery is chosen as a subfield of grammar engineering to illustrate the developed concepts. Grammar recovery is concerned with the derivation of a language's grammar from some available resource such as a semi-formal language reference.
---
paper_title: Compiler test case generation methods: a survey and assessment

paper_content:

Abstract Software testing is an important and critical phase of the application software development life cycle. Testing is a time consuming and costly stage that requires a high degree of ingenuity. In the development stages of safety-critical and dependable computer software such as language compilers and real-time embedded software, testing activities consume about 50% of the project time. In this work we address the area of compiler testing. The aim of compiler testing is to verify that the compiler implementation conforms to its specifications, which is to generate an object code that faithfully corresponds to the language semantic and syntax as specified in the language documentation. A compiler should be carefully verified before its release, since it has to be used by many users. Finding an optimal and complete test suite that can be used in the testing process is often an exhaustive task. Various methods have been proposed for the generation of compiler test cases. Many papers have been published on testing compilers, most of which address classical programming languages. In this paper, we assess and compare various compiler testing techniques with respect to some selected criteria and also propose some new research directions in compiler testing of modem programming languages.
---
paper_title: A sentence generator for testing parsers

paper_content:

A fast algorithm is given to produce a small set of short sentences from a context free grammar such that each production of the grammar is used at least once. The sentences are useful for testing parsing programs and for debugging grammars (finding errors in a grammar which causes it to specify some language other than the one intended). Some experimental results from using the sentences to test some automatically generated simpleLR(1) parsers are also given.
---
paper_title: Uniform random generation of huge metamodel instances

paper_content:

The size and the number of models is drastically increasing, preventing organizations from fully exploiting Model Driven Engineering benefits. Regarding this problem of scalability, some approaches claim to provide mechanisms that are adapted to numerous and huge models. The problem is that those approaches cannot be validated as it is not possible to obtain numerous and huge models and then to stress test them. ::: ::: In this paper, we face this problem by proposing a uniform generator of huge models. Our approach is based on the Boltzmann method, whose two main advantages are its linear complexity which makes it possible to generate huge models, and its uniformity, which guarantees that the generation has no bias.
---
paper_title: USE: A UML-based specification environment for validating UML and OCL

paper_content:

The Unified Modeling Language (UML) is accepted today as an important standard for developing software. UML tools however provide little support for validating and checking models in early development phases. There is also no substantial support for the Object Constraint Language (OCL). We present an approach for the validation of UML models and OCL constraints based on animation and certification. The USE tool (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production.
---
paper_title: Boltzmann Samplers for the Random Generation of Combinatorial Structures

paper_content:

This article proposes a surprisingly simple framework for the random generation of combinatorial configurations based on what we call Boltzmann models. The idea is to perform random generation of possibly complex structured objects by placing an appropriate measure spread over the whole of a combinatorial class – an object receives a probability essentially proportional to an exponential of its size. As demonstrated here, the resulting algorithms based on real-arithmetic operations often operate in linear time. They can be implemented easily, be analysed mathematically with great precision, and, when suitably tuned, tend to be very efficient in practice.
---
paper_title: The category-partition method for specifying and generating fuctional tests

paper_content:

An apparatus for recovering pulse-code modulated digital data from a readback signal has equipment for partially equalizing the readback signal, and equipment for completing the partial equalization of the readback signal and for detecting the digital data. The latter equipment includes a delay device for delaying the partially equalized readback signal, equipment for providing a relatively undelayed version of the readback signal, and a differential amplifier for providing a digital signal corresponding to the difference between the delayed readback signal and the relatively undelayed version of the readback signal. The delay device includes a filter for completing the above mentioned partial equalization with the aid of the equipment for providing the relatively undelayed version of the readback signal and the mentioned differential amplifier.
---
paper_title: Validating UML and OCL models in USE by automatic snapshot generation

paper_content:

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model.
---
paper_title: Metamodel-based Test Generation for Model Transformations: an Algorithm and a Tool

paper_content:

In a Model-Driven Development context (MDE), model transformations allow memorizing and reusing design know-how, and thus automate parts of the design and refinement steps of a software development process. A model transformation program is a specific program, in the sense it manipulates models as main parameters. Each model must be an instance of a "metamodel", a metamodel being the specification of a set of models. Programming a model transformation is a difficult and error-prone task, since the manipulated data are clearly complex. In this paper, we focus on generating input test data (called test models) for model transformations. We present an algorithm to automatically build test models from a metamodel.
---
paper_title: Qualifying input test data for model transformations

paper_content:

Model transformation is a core mechanism for model-driven engineering (MDE). Writing complex model transformations is error-prone, and efficient testing techniques are required as for any complex program development. Testing a model transformation is typically performed by checking the results of the transformation applied to a set of input models. While it is fairly easy to provide some input models, it is difficult to qualify the relevance of these models for testing. In this paper, we propose a set of rules and a framework to assess the quality of given input models for testing a given transformation. Furthermore, the framework identifies missing model elements in input models and assists the user in improving these models.
---
paper_title: Uniform random generation of huge metamodel instances

paper_content:

The size and the number of models is drastically increasing, preventing organizations from fully exploiting Model Driven Engineering benefits. Regarding this problem of scalability, some approaches claim to provide mechanisms that are adapted to numerous and huge models. The problem is that those approaches cannot be validated as it is not possible to obtain numerous and huge models and then to stress test them. ::: ::: In this paper, we face this problem by proposing a uniform generator of huge models. Our approach is based on the Boltzmann method, whose two main advantages are its linear complexity which makes it possible to generate huge models, and its uniformity, which guarantees that the generation has no bias.
---
paper_title: USE: A UML-based specification environment for validating UML and OCL

paper_content:

The Unified Modeling Language (UML) is accepted today as an important standard for developing software. UML tools however provide little support for validating and checking models in early development phases. There is also no substantial support for the Object Constraint Language (OCL). We present an approach for the validation of UML models and OCL constraints based on animation and certification. The USE tool (UML-based Specification Environment) supports analysts, designers and developers in executing UML models and checking OCL constraints and thus enables them to employ model-driven techniques for software production.
---
paper_title: UML2ALLOY: A tool for lightweight modelling of discrete event systems

paper_content:

Alloy is a textual language developed by Daniel Jackson and his team at MIT. It is a formal language, which has a succinct syntax and allows specification and automatic analysis of a wide variety of systems. On the other hand, the Unified Modelling Language (UML) is a semi-formal language, which is accepted by the software engineering community as the defacto standard for modelling, specification and implementation of Object based systems. This paper studies the integration of the UML and Alloy into a single CASE tool, which aims to take advantage of the positive aspect of both the UML and Alloy. Alloy and UML specification provide two views of the system. In order to synchronise the two views, we make use of the MDA style transformation. In particular, we shall present a Meta Object Facility (MOF) compliant metamodel for Alloy and define a model transformation from the UML metamodel to the Alloy metamodel. Based on the approach presented in the paper, we have implemented a tool called UML2Alloy for the modelling and analysis of Discrete Event Systems. To evaluate the tool, the paper presents a case study involving the modelling and analysis of a prototype manufacturing system.
---
paper_title: An Extensible SAT-solver

paper_content:

In this article, we present a small, complete, and efficient SAT-solver in the style of conflict-driven learning, as exemplified by Chaff. We aim to give sufficient details about implementation to enable the reader to construct his or her own solver in a very short time.This will allow users of SAT-solvers to make domain specific extensions or adaptions of current state-of-the-art SAT-techniques, to meet the needs of a particular application area. The presented solver is designed with this in mind, and includes among other things a mechanism for adding arbitrary boolean constraints. It also supports solving a series of related SAT-problems efficiently by an incremental SAT-interface.
---
paper_title: A Metamodel for the Measurement of Object-Oriented Systems: An Analysis using Alloy

paper_content:

This paper presents a MOF-compliant metamodel for calculating software metrics and demonstrates how it is used to generate a metrics tool that calculates coupling and cohesion metrics. We also describe a systematic approach to the analysis of MOF-compliant metamodels and illustrate the approach using the presented metamodel. In this approach, we express the metamodel using UML and OCL and harness existing automated tools in a framework that generates a Java implementation and an Alloy specification of the metamodel, and use this both to examine the metamodel constraints, and to generate instantiations of the metamodel. Moreover, we describe how the approach can be used to generate test data for any software based on a MOF-compliant metamodel. We extend our framework to support this approach and use it to generate a test suite for the metrics calculation tool that is based on our metamodel.
---
paper_title: Alloy: a lightweight object modelling notation

paper_content:

Alloy is a little language for describing structural properties. It offers a declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints and yet amenable to a fully automatic semantic analysis. Its meaning is given by translation to an even smaller (formally defined) kernel. This paper presents the language in its entirety, and explains its motivation, contributions and deficiencies.
---
paper_title: EMFtoCSP: A tool for the lightweight verification of EMF models

paper_content:

The increasing popularity of MDE results in the creation of larger models and model transformations, hence converting the specification of MDE artefacts in an error-prone task. Therefore, mechanisms to ensure quality and absence of errors in models are needed to assure the reliability of the MDE-based development process. Formal methods have proven their worth in the verification of software and hardware systems. However, the adoption of formal methods as a valid alternative to ensure model correctness is compromised for the inner complexity of the problem. To circumvent this complexity, it is common to impose limitations such as reducing the type of constructs that can appear in the model, or turning the verification process from automatic into user assisted. Since we consider these limitations to be counterproductive for the adoption of formal methods, in this paper we present EMFtoCSP, a new tool for the fully automatic, decidable and expressive verification of EMF models that uses constraint logic programming as the underlying formalism.
---
paper_title: Automatic Model Generation Strategies for Model Transformation Testing

paper_content:

Testing model transformations requires input models which are graphs of inter-connected objects that must conform to a meta-model and meta-constraints from heterogeneous sources such as well-formedness rules, transformation pre-conditions, and test strategies. Manually specifying such models is tedious since models must simultaneously conform to several meta-constraints. We propose automatic model generation via constraint satisfaction using our tool Cartier for model transformation testing. Due to the virtually infinite number of models in the input domain we compare strategies based on input domain partitioning to guide model generation. We qualify the effectiveness of these strategies by performing mutation analysis on the transformation using generated sets of models. The test sets obtained using partitioning strategies gives mutation scores of up to 87% vs. 72% in the case of unguided/random generation. These scores are based on analysis of 360 automatically generated test models for the representative transformation of UML class diagram models to RDBMS models.
---
paper_title: The Sat4j library, release 2.2

paper_content:

Sat4j is a mature, open source library of SAT-based solvers in Java. It provides a modular SAT solver architecture designed to work with generic constraints. Such architecture is used to provide SAT, MaxSat and pseudo-boolean and solvers for lightweight constraint programming. Those solvers have been evaluated regularly in the corresponding international competitive events. The library has been adopted by several academic softwares and the widely used Eclipse platform, which relies on a pseudo-boolean solver from Sat4j for its plugins dependencies management since June 2008.
---
paper_title: Validating UML and OCL models in USE by automatic snapshot generation

paper_content:

We study the testing and certification of UML and OCL models as supported by the validation tool USE. We extend the available USE features by introducing a language for defining properties of desired snapshots and by showing how such snapshots are generated. Within the approach, it is possible to treat test cases and validation cases. Test cases show that snapshots having desired properties can be constructed. Validation cases show that given properties are consequences of the original UML and OCL model.
---
paper_title: UML2Alloy: A Challenging Model Transformation

paper_content:

Alloy is a formal language, which has been applied to modelling of systems in a wide range of application domains. It is supported by Alloy Analyzer, a tool, which allows fully automated analysis. As a result, creating Alloy code from a UML model provides the opportunity to exploit analysis capabilities of the Alloy Analyzer to discover possible design flaws at early stages of the software development. Our research makes use of model based techniques for the automated transformation of UML class diagrams with OCL constraints to Alloy code. The paper demonstrates challenging aspects of the model transformation, which originate in fundamental differences between UML and Alloy. We shall discuss some of the differences and illustrate their implications on the model transformation process. The presented approach is explained via an example of a secure e-business system.
---
paper_title: Alcoa: the alloy constraint analyzer

paper_content:

Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other end, it embodies a lightweight formal method in which subtle properties of behaviour can be investigated. Alcoa's input language, Alloy, is a new notation based on Z. Its development was motivated by the need for a notation that is more closely tailored to object models (in the style of UML), and more amenable to automatic analysis. Like Z, Alloy supports the description of systems whose state involves complex relational structure. State and behavioural properties are described declaratively, by conjoining constraints. This makes it possible to develop and analyze a model incrementally, with Alcoa investigating the consequences of whatever constraints are given. Alcoa works by translating constraints to boolean formulas, and then applying state-of-the-art SAT solvers. It can analyze billions of states in seconds.
---
paper_title: Metamodel-based Test Generation for Model Transformations: an Algorithm and a Tool

paper_content:

In a Model-Driven Development context (MDE), model transformations allow memorizing and reusing design know-how, and thus automate parts of the design and refinement steps of a software development process. A model transformation program is a specific program, in the sense it manipulates models as main parameters. Each model must be an instance of a "metamodel", a metamodel being the specification of a set of models. Programming a model transformation is a difficult and error-prone task, since the manipulated data are clearly complex. In this paper, we focus on generating input test data (called test models) for model transformations. We present an algorithm to automatically build test models from a metamodel.
---
paper_title: Extensive validation of OCL models by integrating SAT solving into USE

paper_content:

The Object Constraint Language (OCL) substantially enriches modeling languages like UML, MOF or EMF with respect to formulating meaningful model properties. In model-centric approaches, an accurately defined model is a requisite for further use. During development of a model, continuous validation of properties and feedback to developers is required, since many design flaws can then be directly discovered and corrected. For this purpose, lightweight validation approaches which allow developers to perform automatic model analysis are particularly helpful. We provide a new method for efficiently searching for model instances. The existence or non-existence of model instances with certain properties allows significant conclusions about model properties. Our approach is based on the translation of UML and OCL concepts into relational logic and its realization with SAT solvers. We explain various use cases of our proposal, for example, completion of partly defined model instances so that particular properties hold in the completed model instances. Our proposal is realized by integrating a model validator as a plugin into the UML and OCL tool USE
---
paper_title: Qualifying input test data for model transformations

paper_content:

Model transformation is a core mechanism for model-driven engineering (MDE). Writing complex model transformations is error-prone, and efficient testing techniques are required as for any complex program development. Testing a model transformation is typically performed by checking the results of the transformation applied to a set of input models. While it is fairly easy to provide some input models, it is difficult to qualify the relevance of these models for testing. In this paper, we propose a set of rules and a framework to assess the quality of given input models for testing a given transformation. Furthermore, the framework identifies missing model elements in input models and assists the user in improving these models.
---
paper_title: UML2ALLOY: A tool for lightweight modelling of discrete event systems

paper_content:

Alloy is a textual language developed by Daniel Jackson and his team at MIT. It is a formal language, which has a succinct syntax and allows specification and automatic analysis of a wide variety of systems. On the other hand, the Unified Modelling Language (UML) is a semi-formal language, which is accepted by the software engineering community as the defacto standard for modelling, specification and implementation of Object based systems. This paper studies the integration of the UML and Alloy into a single CASE tool, which aims to take advantage of the positive aspect of both the UML and Alloy. Alloy and UML specification provide two views of the system. In order to synchronise the two views, we make use of the MDA style transformation. In particular, we shall present a Meta Object Facility (MOF) compliant metamodel for Alloy and define a model transformation from the UML metamodel to the Alloy metamodel. Based on the approach presented in the paper, we have implemented a tool called UML2Alloy for the modelling and analysis of Discrete Event Systems. To evaluate the tool, the paper presents a case study involving the modelling and analysis of a prototype manufacturing system.
---
paper_title: Fundamentals of Algebraic Graph Transformation

paper_content:

This is the first textbook treatment of the algebraic approach to graph transformation, based on algebraic structures and category theory. It contains an introduction to classical graphs. Basic and advanced results are first shown for an abstract form of replacement systems and are then instantiated to several forms of graph and Petri net transformation systems. The book develops typed attributed graph transformation and contains a practical case study.
---
paper_title: A Metamodel for the Measurement of Object-Oriented Systems: An Analysis using Alloy

paper_content:

This paper presents a MOF-compliant metamodel for calculating software metrics and demonstrates how it is used to generate a metrics tool that calculates coupling and cohesion metrics. We also describe a systematic approach to the analysis of MOF-compliant metamodels and illustrate the approach using the presented metamodel. In this approach, we express the metamodel using UML and OCL and harness existing automated tools in a framework that generates a Java implementation and an Alloy specification of the metamodel, and use this both to examine the metamodel constraints, and to generate instantiations of the metamodel. Moreover, we describe how the approach can be used to generate test data for any software based on a MOF-compliant metamodel. We extend our framework to support this approach and use it to generate a test suite for the metrics calculation tool that is based on our metamodel.
---
paper_title: Automatic Model Generation Strategies for Model Transformation Testing

paper_content:

Testing model transformations requires input models which are graphs of inter-connected objects that must conform to a meta-model and meta-constraints from heterogeneous sources such as well-formedness rules, transformation pre-conditions, and test strategies. Manually specifying such models is tedious since models must simultaneously conform to several meta-constraints. We propose automatic model generation via constraint satisfaction using our tool Cartier for model transformation testing. Due to the virtually infinite number of models in the input domain we compare strategies based on input domain partitioning to guide model generation. We qualify the effectiveness of these strategies by performing mutation analysis on the transformation using generated sets of models. The test sets obtained using partitioning strategies gives mutation scores of up to 87% vs. 72% in the case of unguided/random generation. These scores are based on analysis of 360 automatically generated test models for the representative transformation of UML class diagram models to RDBMS models.
---
paper_title: Towards an automated test generation for the verification of model transformations

paper_content:

It is widely accepted that model transformations play an important role in the MDA approach. As for any software, the validation and verification are essential in the life cycle of a model transformation. The proposition of an automatic approach that is based on functional testing techniques for the verification of model transformations reveals three main issues: the automatic generation of test data, the verification criteria, and the definition of the test oracle. The scope of this paper is restricted to the automatic generation of test data issue of the verification process. We first present a background on essential methods for test case generation and we argue their adaptation for the verification of model transformations. For an automated generation of test data we propose a formal language to be used for the specification of model transformations. We also propose a data partitioning technique that focuses on the structure of models in order to take into account the structural aspect of models when generating input test models. Our partitioning technique is to be combined with existing techniques to cover the whole characteristics of the value a model.
---
paper_title: Translation of Restricted OCL Constraints into Graph Constraints for Generating Meta Model Instances by Graph Grammars

paper_content:

The meta modeling approach to syntax definition of visual modeling techniques has gained wide acceptance, especially by using it for the definition of UML. Since meta-modeling is non-constructive, it does not provide a systematic way to generate all possible meta model instances. In our approach, an instance-generating graph grammar is automatically created from a given meta model. This graph grammar ensures correct typing and cardinality constraints, but OCL constraints for the meta model are not supported yet. To satisfy also the given OCL constraints, well-formedness checks have to be done in addition. We present a restricted form of OCL constraints that can be translated to graph constraints which can be checked during the instance generation process.
---
paper_title: UML2Alloy: A Challenging Model Transformation

paper_content:

Alloy is a formal language, which has been applied to modelling of systems in a wide range of application domains. It is supported by Alloy Analyzer, a tool, which allows fully automated analysis. As a result, creating Alloy code from a UML model provides the opportunity to exploit analysis capabilities of the Alloy Analyzer to discover possible design flaws at early stages of the software development. Our research makes use of model based techniques for the automated transformation of UML class diagrams with OCL constraints to Alloy code. The paper demonstrates challenging aspects of the model transformation, which originate in fundamental differences between UML and Alloy. We shall discuss some of the differences and illustrate their implications on the model transformation process. The presented approach is explained via an example of a secure e-business system.
---
paper_title: Metamodel-based Test Generation for Model Transformations: an Algorithm and a Tool

paper_content:

In a Model-Driven Development context (MDE), model transformations allow memorizing and reusing design know-how, and thus automate parts of the design and refinement steps of a software development process. A model transformation program is a specific program, in the sense it manipulates models as main parameters. Each model must be an instance of a "metamodel", a metamodel being the specification of a set of models. Programming a model transformation is a difficult and error-prone task, since the manipulated data are clearly complex. In this paper, we focus on generating input test data (called test models) for model transformations. We present an algorithm to automatically build test models from a metamodel.
---
paper_title: Qualifying input test data for model transformations

paper_content:

Model transformation is a core mechanism for model-driven engineering (MDE). Writing complex model transformations is error-prone, and efficient testing techniques are required as for any complex program development. Testing a model transformation is typically performed by checking the results of the transformation applied to a set of input models. While it is fairly easy to provide some input models, it is difficult to qualify the relevance of these models for testing. In this paper, we propose a set of rules and a framework to assess the quality of given input models for testing a given transformation. Furthermore, the framework identifies missing model elements in input models and assists the user in improving these models.
---

Title: Metamodel Instance Generation: A Systematic Literature Review

Section 1: Introduction
Description 1: Introduce the context of the study and explain the importance of metamodels in model-driven engineering. Highlight the need for metamodel instance generation and provide an overview of the paper's structure.

Section 2: Background
Description 2: Discuss the concept of metamodeling, its advantages, and its limitations, particularly in the context of test case generation. Outline the research questions addressed in the paper.

Section 3: Review Research Methods
Description 3: Describe the methodologies used for searching, selecting, and assessing the studies included in the literature review. Explain the process of forming search terms and the search strategy.

Section 4: Search Terms
Description 4: Detail the search terms derived from research questions, various representations of metamodels, and constraint management techniques.

Section 5: Paper Selection Study
Description 5: Explain the paper selection process, including the criteria for judging papers based on their titles, abstracts, and content. Summarize the number of papers chosen for detailed study.

Section 6: Selected Papers
Description 6: Present the selected papers in a categorized manner, detailing the main ideas and contributions of each paper.

Section 7: Discussion
Description 7: Discuss the findings from the selected papers by answering the research questions. Analyze the main areas related to metamodel instance generation, the algorithms and theoretical frameworks used, the selection criteria for instances, and the tools available for instance generation.

Section 8: Summary
Description 8: Summarize the key insights gained from the literature review. Highlight the main techniques and tools discussed and their advantages and limitations.

Section 9: Conclusion
Description 9: Conclude the paper by summarizing the main contributions of the systematic literature review and identifying potential future research directions.

Section 10: References
Description 10: List all the references cited throughout the paper.