The engineering of hierarchically decomposed component-based systems emphasizes the separation of concerns to reduce development complexity through work distribution and component reuse. Variability further promotes reuse, as system variants may be used in different markets or contexts. However, variability must be adequately managed as it introduces another layer of complexity to system development. Consequently, modeling of hierarchical component-based systems should support composition of variable components while simultaneously facilitating their formal analysis. To address this, we formally define variable component types, propose a modeling language for specifying the variability of hierarchically composed systems, and present a method to check the component variants' well-formedness. We extend the semantically grounded architecture description language MontiArc to realize the modeling of variable component-based systems supporting the well-for medness of variable component types and late binding of variability. The resulting realization of variable component types enables the specification of reusable and flexible components while making customization options explicit in the component interface and maintaining the black-box view of components. This can ultimately reduce complexity in developing variable components and, thus, facilitate the engineering of component-based systems.
When model-driven engineering is applied to critical systems, proving the correctness of model transformations (MT) assumes great importance. For instance, users may want a guarantee that the transformation does not produce models that break a critical post-condition, or that it preserves the semantics of the transformed model. Methods for automatic proof of MT correctness have shown their effectiveness for simple transformations and/or correctness properties. However, arbitrarily complex transformations and properties may require interactive theorem proving, that is a very costly activity. In this paper we aim at simplifying the development of interactive proofs for MTs written in the CoqTL transformation language, by providing a set of automated proof tactics for MT certification. The tactics encode reasoning patterns that depend only on the semantics of the CoqTL engine, hence they are generally applicable to proofs on any CoqTL transformation. Each tactic is associated to a direction (forward if it derives facts about the target model given facts on the source model, backward if it derives facts on the source given facts on the target) and a subject (element or link, respectively if the tactic derives facts on elements or links). They are implemented as a set of lemmas and tactics for the Coq interactive theorem prover. In our experimentation, we show that these tactics allows us to write shorter and easier proofs.
Nowadays, iterative development has become a state-of-the-art engineering process. The shared artifacts, i.e., models, must be edited collaboratively to make iterative development work in large engineering teams. The typical non-real-time collaboration workflow consists of three phases: The collaborators create copies of the model; Each collaborator edits their variant (copy) of the model; The collaborators merge the edited models back into one. During the merge phase, conflicting changes become apparent and must be resolved. This is a time and resource-intensive task. However, if potential merge conflicts can be detected during the editing phase, the collaborators can take suitable measures in time. This work proposes an early warning system for merge conflicts in model-based development projects. We introduce the novel metric Drift to quantify the inconsistency between all co-existing variants of a model. An increase in Drift indicates an increase in potential merge conflicts. We evaluate the correctness of the Drift for synthetical modeling projects and syntactical model differences. We develop an openly available tool for calculating the Drift for arbitrary Git repositories.
In software engineering reference models are used as a guidance for implementing potential solutions to recurring problems, e.g., as reference architecture models or reference data models. Despite the broad use of reference models in practice, there is no clear definition for what it means that a concrete model conforms to a reference model. This prevents us from developing automated tools for conformance checking. In this paper, we provide a semantically useful definition of conformance of concrete models to reference models. We then present concepts and tools for concrete automated conformance checks for (1) class diagrams, (2) feature diagrams, and (3) state charts, which we developed based on that definition. Finally, we discuss (1) the commonalities and differences of the presented automated conformance checks and (2) general design considerations for developing reference model conformance checkers in the context of model-driven engineering. Key findings are that reference models should use the same language as their concrete models, conformance checks require conformance mappings between reference and concrete model elements, and conformance rules must be based on formally defined language semantics.
Metamodels play an important role in MDE and in specifying a software language. They are cornerstone to generate other artifacts of lower abstraction level, such as code. Developers then enrich the generated code to build their language services and tooling, e.g., editors, and checkers. When a metamodel evolves, part of the code is regenerated and all the additional developers' code can be impacted. Thus, requiring erroneous code to be co-evolved accordingly. In this paper, we explore a novel approach to mitigate the challenge of metamodel evolution impacts on the code using LLMs. In fact LLMs stand as promising tools for tackling increasingly complex problems and support developers in various tasks of writing, correcting and documenting source code, models, and other artifacts. However, while there is an extensive empirical assessment of the LLMs capabilities in generating models, code and tests, there is a lack of work on their ability to support their maintenance. In this paper, we focus on the particular problem of metamodels and code co-evolution. We first designed a prompt template structure that contains contextual information about metamodel changes, the abstraction gap between the metamodel and the code, and the erroneous code to co-evolve. To investigate the usefulness of this template, we generated three more variations of the prompts. The generated prompts are then given to the LLM to co-evolve the impacted code. We evaluated our generated prompts and other three of their variations with ChatGPT version 3.5 on seven Eclipse projects from OCL and Modisco evolved metamodels. Results show that ChatGPT can co-evolve correctly 88.7 % of the errors due to metamodel evolution, varying from 75% to 100% of correctness rate. When varying the prompts, we observed increased correctness in two variants and decreased correctness in another variant. We also observed that varying the temperature hyperparameter yields better results with lower temperatures. Our results are observed on a total of 5320 generated prompts. Finally, when compared to the quick fixes of the IDE, the generated prompts co-evolutions completely outperform the quick fixes.
