\newcontent{Modeling and model-driven processes offer abstraction to cope with the increasing complexity of systems. Since federated models describe overlapping aspects of the same system, some information is shared, introducing redundancy. Maintaining consistency of such information is crucial to ensure a coherent system representation. In safety-critical domains, such consistency requirements often require formal verification to ensure strong correctness guarantees. However, the verification effort is influenced not only by the models themselves, but also by the structure and expressiveness of the consistency specifications. In this article, we examine the complexity of consistency from a formal perspective. We embed OCL-based consistency constraints into higher-order logic using the theorem prover Isabelle/HOL and analyze the resulting proof obligations. By identifying key dimensions that influence the verification effort, we aim to understand how the design of consistency specifications affects the formal reasoning required to assess them.We illustrate the approach via a case study of a car braking system, for which we construct a mechanized formalization of realistic metamodels and consistency constraints, and discuss metrics for their proof complexity. Understanding which structural aspects of consistency influence the verification effort provides a foundation for ultimately reducing unnecessary complexity while ensuring the required consistency constraint.}
Maintaining consistency between related models is achieved through Consistency Preservation Rules (CPRs) that propagate changes from a source model to a target model. However, in many cases, additional input from the maintainer of a target model, based on their domain knowledge, is required to integrate changes into target models. Therefore, the change cannot be propagated automatically and introduces temporary inconsistency. To manage the temporary inconsistency, we propose CoCoPath, a concolic execution framework for systematically exploring execution paths in consistency-preserving model transformations. We combine dynamic taint tracking, concolic execution, and model transformation frameworks to derive potential target models based on the source model, the consistency preservation rules, and optional domain constraints to further restrict the search space. By comparing these alternative target models, users can explore the consequences of different additional inputs and resolve temporary inconsistency in an informed manner. We validate our contribution by applying our approach to an industry case study, showcasing its capabilities for one and multiple awaited user inputs.
Software architectures are not only the foundation on which software systems are built, but also provide a basis for reasoning about system properties, such as security, even before the first line of code is written. A software architecture is shaped by a set of design decisions made by architects. For a given design problem, multiple decisions are often possible, and selecting any one of them leads to a different design alternative, each of which introduces a different attack surface. Despite the significant impact of architectural design decisions on the security of the implemented system, a systematic method for assessing security during the architecture design stage remains an open challenge. To improve support here, we propose a metamodel extension to an existing architectural description language, in order to include the security zones of the system, i.e., modeling where system users can interact with the deployed system. We utilize this information to propose a new approach for generating abstract penetration test cases for scenarios in which the boundaries between zones are crossed. In this paper, we consider information-flow analysis as a concrete application area of security assessment. Consequently, a zone crossing in this context corresponds to a location where confidential information might be leaked. The generated test cases can then be used to detect potential leakage of confidential information, either at design time or during late penetration testing, once the system is deployed. We evaluate the approach using the Goal-Question-Metric (GQM) method across five case studies, considering usefulness, effort reduction, and performance. The results indicate that the generated abstract penetration test cases (APTCs) are mostly useful for architecture-level security assessment and can guide later penetration testing, while supporting effort reduction and requiring only low runtime overhead.
The deployment of modern containerized architectures depends on container orchestration tools, because their configuration critically influence performance, robustness, and cost. Container orchestration tools manage scaling, health checking, failure recovery, and resource distribution among containers. Configuration evaluation as well as suitability of container orchestration are nontrivial at design time, not to mention expensive. For informed decision-making in container architectures, modeling and simulation provide lightweight alternatives.In this paper, we present a novel approach to modeling and simulating dynamic container architectures. Implemented as an extension of the Palladio Component Model, our approach captures essential orchestration mechanisms such as autoscaling, container scheduling, and the configuration of requests and limits. Our qualitative evaluation uses two example applications and load scenarios. The results show that our approach closely simulates dynamic containerized architectures while enabling lightweight comparison between different configurations and traditional deployment techniques.
Component-based software architecture enables software architects to design complex systems by composing components that interact through well-defined, syntactically specified interfaces. A special kind of component we investigated in our previous work is the analysis components. Analysis components support the evaluation and prediction of system's functional and non-functional properties. Evaluating these properties early in the development process helps optimize system performance and ensure compliance with requirements. While approaches for modeling and analyzing such systems, such as the Palladio approach, support syntactic validation of the composition, they often lack mechanisms to ensure the semantic soundness of compositions. In this paper, we present a model transformation approach to help architects ensure that system models are semantically sound and behave as expected. This approach enables the transformation of Palladio models into MontiArc models, allowing architects to enrich their system representations with semantic constraints and validate these constraints with the MontiArc workbench. This ensures that component interactions are consistent with both structural composition and intended semantics. We evaluate our approach through two different case studies. From these case studies, we derived several scenarios with varying constraints and states to assess the accuracy and performance of our approach. To evaluate accuracy, we examined our approach's ability to check semantic constraints and detect violations. We observed high accuracy across the case studies. For performance, we analyze time complexity in different constraint types. The approach performed well when applied to arithmetic constraints, with its effectiveness decreasing when applied to more complex string-centered constraints.
Model-Based Systems Engineering (MBSE) is seen as a way of addressing the complexity of traditional document-centric development in Systems Engineering (SE). MBSE offers easier formalization of knowledge, higher abstraction, and tool support, allowing automated analysis and integration of artifacts across different domains. However, the adoption of MBSE is hindered by the need for manually creating new models in semi-formal languages like SysML, which should cover all domains. Thus, a different modeling principle, like Multi-Level Modeling (MULTI), could ease the creation of different models, as MULTI enables modelers to abstract concepts over more than just one model. In this paper, we explore MULTI as a modeling paradigm for MBSE by applying it to a running example from the Construction Equipment (CE) domain. We analyze and contrast MULTI to the existing modeling implementation. We conclude that the MULTI paradigm opens MBSE to support traceability, re-use, verifiable design documents, and may improve communication with stakeholders. Further, we discuss future applications of MULTI and how it might be transferred to industrial settings.
We contribute a solution to the Model Management (MoM) Challenge 2025 (https://doi.org/10.5281/zenodo.15285132) with the Vitruvius framework. Vitruvius manages multiple models in a so-called Virtual Single Underlying Model. It maintains consistency between models through preservation rules written in a custom Domain-Specific Language, and projects views defined via view types to interact with the modeled system. We define Metamodels to model the part catalog, system architecture, and satellite requirements in the challenge. Between the part catalog and system architectures, we also define Consistency Preservation Rules. Finally, we construct a view type that generates reports as views. With these components, our Virtual Single Underlying Model handles the first three scenarios of the challenge. In this paper, we also detail our plans to support versioning and collaboration in Vitruvius. We preview future developments, and compare Vitruvius to other model management approaches.
Modeling and model-driven processes offer abstraction as a means to cope with the increasing complexity of systems. As systems become more complex, additional stakeholders with diverse expertise contribute, leading to heterogeneous and federated models, each capturing a different perspective and abstraction. Since these models describe overlapping aspects of the same system, some information is shared, and thus redundancy is introduced. Maintaining consistency of such information across models is crucial to ensure that they collectively provide a coherent system representation. In fact, inconsistencies can lead to errors in system development, making consistency necessary for system correctness. In addition, when the system is critical to safety, the correctness must be established with the highest level of guarantee, for example, achieved by formal verification. In this context, understanding which aspects of the consistency’s complexity influence the complexity of verification may allow for more efficient verification techniques. In this paper, we examine the complexity of consistency for managing and mitigating verification efforts, to ultimately systematically reduce unnecessary complexity while ensuring the required consistency.
Models and metamodels change, entailing efforts to keep related artifacts consistent, i.e., to reflect the implications of the changes on them. In order to assess these implications, the changes or evolution steps themselves are, in most cases, of highest interest, compared to the states of the models or metamodels. While the states can be used to derive the changes, some information on the actual changes might get lost, e.g., whether an empty class has been renamed or deleted and re-added. The use of deltas to describe changes is not limited to models and metamodels, but is also employed in other research areas. To get an overview of the used concepts and how they compare, we did a scoping literature review in the field of computer science, focused on modeling and related fields. We compared the different approaches in regard to how they model the change, their ability to model atomic or composite changes, their completeness in modeling all possible changes, as well as their purpose. This overview allows for more efficient concept re-use across domains in regard to the modeling of changes and the different use cases realized with them.
At its very core, model-based systems engineering uses models to enable a multidisciplinary view on a system design in the early stages. These early stage models evolve horizontally: new diagrams for further perspectives and disciplines are added, using the same notation and the same abstraction level. Just as any other process in systems engineering, horizontal model evolution is subject to guidelines and standards, and the multidisciplinary view on a horizontal evolution, involving at least two disciplines, requires referring to multiple guidelines. Despite the significant effort invested in this process, there is no framework or tool support for engineering reviews of horizontal model evolution. In this paper, we aim to support engineering reviews by providing traceability for engineering activities that evolve a model horizontally. Our contribution is a process-agnostic framework that relies on capturing the intent of model changes in addition to the changes themselves. We group the model changes into transactional units called deltas, which are subsequently annotated with the engineer's intent to perform these specific changes. We give a methodology to integrate such intent-annotated deltas into engineering reviews and audits, an ontology to capture intent, and a meta-model for the deltas to achieve a language- and guideline-independent framework. We use an example from the earth moving machinery domain to exemplify the need for horizontal model evolution and provide a prototypical proof-of-concept implementation in the SysML Papyrus Plugin for Eclipse and a SysML case study using a machine brake system.
In an increasingly digital and interconnected world, cross-domain collaboration is essential for building sustainable and adaptable systems. This paper explores how concepts already implemented in one domain can be transferred into the languages used in another domain to support the customization of domain-specific modeling languages. We propose a methodology for this domain-tuning of languages by identifying and leveraging overlapping concept needs between domains. We demonstrate the applicability of our approach through the transfer of the concept of consistency from database management systems to model-driven engineering, mapping, e.g., the concepts of primary keys from databases to model element identity. Our proposed approach enables the fine-tuning of modeling languages to better align with the needs of specific application domains by re-using existing language concepts across the borders of domains. The result is an exploratory language engineering process that enhances the integration and expressiveness of modeling languages by crossing domain boundaries. We plan to apply our approach to other domains to gain further insights into its applicability.
Modern engineering systems often require collaboration across multiple domains, each using different models and tools. By implementing automated processes for keeping consistency, changes propagate across these models and tools, affecting the work of various stakeholders and teams. However, an explanation of these automatically propagated changes is often required. This paper presents a case study using heterogeneous models in the development and validation of a crossdomain automotive brake system. Our case study comprises a Brake Specification Model, a Computer-Aided Design Model, a Simulation Model as well as their corresponding metamodels, and a model of a real-world test bench for brake validation. We also present a set of change and explainability scenarios that occur during the development and validation process of a cyber-physical brake system. We use these scenarios to highlight the explainability requirements and challenges which should be addressed by any explainability solutions and approaches for cross-domain engineering and validation processes in the cyber-physical system context. By providing such models and metamodels, as well as the change and explainability scenarios that use them, our work will aid researchers in validating their approaches and in investigating those development challenges which arise from cross-domain consistent cyber-physical systems development.
The complexity of industrial workflows often necessitates the use of multiple models to adequately describe systems at various levels of abstraction. However, as the number of models involved in a process increases, so too does the potential for inconsistencies between models. These inconsistencies can impede workflow completion. Despite existing methods to manage workflows, there is a lack of approaches specifically addressing the modeling of inconsistencies between different models. In this paper, we propose a method to model inconsistencies between models, using specific event types within BPMN 2.0 diagrams, leveraging existing extensions to BPMN 2.0. We applied and evaluated this method in the manufacturing industry, specifically at a precision component manufacturer. We conducted nine expert interviews, and the insights we gained have helped us to identify 13 potential inconsistencies between the models used by the manufacturer. In our evaluation, the proposed modeling approach achieved a good level of usability. Our experience report adds real-world application to this practical solution for managing inconsistencies in industrial workflows. In this way, we contribute both to the field and to the practice of model-based engineering.
In cross-organizational software engineering, every model managed may contain intellectual property (IP). That IP must be protected from potential competitors, who may also be fellow collaborators. To that end, organizations use access control systems to manage access to the parts of a model or the model as a whole as part of their model management efforts. However, access control systems often need to be shared, thereby potentially compromising the IP protection in place. In this paper, we introduce DEBAC, an approach for using the rules of role-based access control to derive encryption rules. We are able to circumvent the sharing of access control systems by using instead the encryption of model deltas (i.e., arbitrary changes to a model). To evaluate our approach, we generate use cases from open source GitHub repositories (committers being regarded as collaborating organizations) and show evidence for the functionality and applicability of the DEBAC approach. With the DEBAC approach, we can derive the encryption rules to be able to store any model on any untrusted infrastructure while still being able to preserve IP.