Model transformation is a core mechanism for Model-Driven Engineering (MDE). Writing complex programs such as model transformations (MT) is error-prone, and efficient testing techniques are required for their quality assurance. There are several challenges when it comes to testing MT, including the automatic generation of suitable input test models and the construction of test oracles based on verification properties. Many approaches to generating input models ensure coverage of a certain level of the source meta-model and some input/output model constraints. Furthermore, most transformation testing techniques are tailored to specific implementation languages or quality properties, which makes it difficult to reuse testing techniques for different languages due to their language-specific nature. The diversity of languages and verification properties raises the need for a black-box testing framework of MT that is independent of transformation implementation languages as well as supports systematic verification of the quality properties. In this paper, we clarify the basic elements of such a framework, and how to apply this framework for systematically testing MT. The main tasks of the model transformation testing process, including test design, test execution and evaluation, are defined and realized within this integrated framework.

Software transactional memory (STM) programs usually use more memory resources than traditional programs. Therefore, estimating an upper bound of memory resources used by an STM program is crucial for optimizing the program and reducing the risks of out-of-memory runtime exceptions. However, due to the complex nesting of transactions and threads, the estimation problem is challenging. In our previous work, we have developed several type systems to address the problem for core imperative languages with STM primitives. This work advances our previous works, in which we add object-oriented constructs to the language while keeping the STM primitives, to make the language closer to practical languages. Then, we built a type system to statically estimate the maximum memory required by well-typed programs of the language.

This paper proposes a transformation-based method to automatically generate functional test cases from use cases named USLTG (Use case Specification Language (USL)-based Test Generation). We first focus on developing a modeling language named Test Case Specification Language (TCSL) in order to express test cases. Test cases in TCSL can contain detailed information including test steps, test objects within steps, actions of test objects, and test data. Such information is often ignored in currently available test case specifications. We then aim to generate test cases in a TCSL model by a transformation from use cases that are represented by a USL. The USLTG transformation includes three main steps in generating (1) scenarios, (2) test data, and (3) a TCSL model. Within our transformation, the OCL solver is employed in order to build system snapshots as the part of test cases and to identify other test data. We applied our method to two case studies and evaluated our method by comparing it with other recent works.

Class models are often employed to represent domains. In order for class models to conform to their intended domain semantics, we need to ensure their precision and consistency. Precision can be achieved by augmenting the models with constraints, and consistency can be achieved by avoiding contradictory constraints. Model finding is a technique to maintain this kind of consistency. It automatically checks the satisfiability of models by using example instances. However, this technique is often inefficient when applied to large models due to the huge search space. In this paper, we propose a technique to narrow the search space by using patterns to represent constraints. Constraint patterns allow us to put further restrictions on the search space. Our case study illustrates that using constraint patterns in this way can improve the verification process.

User Scenarios have been advocated as an effective means to capture requirements by describing the system-to-be at the instance or example level. This instance-level information is then used to infer a possible software specification consistent with the provided valid and invalid scenarios. So far existing approaches have often focused on the generation of static models but have omitted the inference of business rules that could complement the static models and improve the precision of the software specification. In this sense this paper provides a first set of invariant inference patterns that are applied on valid and invalid snapshots in order to generate OCL~(Object Constraint Language) integrity constraints that the system should always satisfy. We strengthen the confidence of inferred results based on the user's feedback of generated examples and counterexamples for the considered constraint. The approach is realized with a prolog-based tool that could support the designer to effectively define OCL integrity constraints in a semi-automatic way.

Presenting precisely models and supporting automatic manipulation of models are at the heart of model-centric software development. A formal foundation for these tasks is a necessity as well as a challenge. We present a model-driven approach based on the integration of two light-weight formal methods, the object constraint language (OCL) and triple graph grammars (TGGs). OCL together with metamodeling allows us to present precisely models. With TGGs we can carry out model manipulations, especially model transformations. We focus on explaining the tool which realizes our approach. This tool is developed as an extension of the UML-based specification environment (USE), which offers full OCL support. A case study showing the transformation between statecharts and extended hierarchical automata explains our approach.