Client Challenge

doi.org

A survey of modeling languages for automotive digital twins - Software and Systems Modeling

The demand for digital twins and suitable modeling techniques in the automotive industry is increasing rapidly. Yet, there is no common understanding of digital twins in automotive, nor are there modeling techniques established to create automotive digital twins. Recent studies on digital twins focus on the analysis of the literature on digital twins for automotive or in general and, thus, neglect the industrial perspective of automotive practitioners. To mitigate this gap between scientific literature and the industrial perspective, we conducted a questionnaire survey among experts in the German automotive industry to identify (i) the desired purposes for and capabilities of digital twins, (ii) the modeling techniques related to engineering and operating digital twins across the phases of automotive development, and (iii) the role informal models play during automotive development. To this end, we contacted 189 members of the Software-Defined Car research project and received 96 responses. The results show that digital twins are considered most useful in the usage and support phase of automotive development, representing vehicles as-operated. Moreover, simulation models, source code, and business process models are currently considered the most important models to be integrated into a digital twin alongside the associated, established tools. Furthermore, informal models are frequently created digitally, e.g., using PowerPoint™, mainly employed for communication and documentation during the conception and development phase.

doi.org

UML4UI: UML as a foundation for model-based and model-driven user interface engineering - Software and Systems Modeling

Model-Based and Model-Driven Engineering provide systematic means to manage the complexity of modern User Interface (UI) development by elevating models to first-class artifacts. Both approaches express multiple abstraction levels of the UI, while the latter uses model transformations to move between them. Both ensure consistency, improve reusability, reduce coding effort, and strengthen traceability across levels. However, several challenges remain. This paper examines the role of the Unified Modeling Language (UML) as a foundational modeling framework for both approaches. We show how UML can be used to (meta-)model presentational, behavioral, and interaction aspects across various abstraction levels, from task and domain models, through abstract and concrete UI specifications, and down to final UIs. Forward engineering produces UIs from models, reverse engineering recovers models from existing UIs, and lateral engineering adapts them to the context of use. Using a running example, we compare Model-Based and Model-Driven Engineering and derive some insights into the practical use of UML to address recurring challenges in UI development. We further provide a comparative discussion of UML-based approaches by reviewing existing work, namely UI Description Languages (UIDLs) as domain-specific modeling notations for UI development. We identify open research challenges that must be addressed to fully leverage UML as a comprehensive and standardized modeling and transformation framework for UI development.

doi.org

Assessing model-driven mutation testing of Java bytecode - Software and Systems Modeling

Mutation testing is an approach to checking the robustness of test suites. The program code is slightly modified by mutations to inject bugs, and a test suite is robust enough if it finds them. Mutation testing tools provide sets of mutation operators, such as swapping arithmetic operators, to make small modifications to the program. The results of mutation tests depend directly on the possible mutations. These mutations should cause actual changes in the program behavior, but also should not prevent the program from being loaded and executed. The more advanced mutations are, the more they challenge the test suite. Existing non-model-based mutation testing tools do not support the definition of advanced mutation operators that go beyond manipulating a small number of adjacent instructions within a single method. Thus, we present a model-driven approach where mutations of Java bytecode can be flexibly defined as model transformations. Our tool, Model-based Mutation Testing (MMT), implements this approach and includes model transformations for conventional and advanced mutation operators, such as deleting overridden methods or changing type casts. To evaluate the effectiveness and efficiency of model-driven mutation testing, we have applied MMT to all projects and versions in Defects4J, a well-established collection of real-world Java projects with reproducible bugs. We check for MMT’s ability to generate mutants close to real bugs and compare it with the non-model-based mutation testing tools Jumble, PIT, and $$\mu $$ μ BERT. Our evaluation shows that MMT and PIT are significantly more effective and efficient than $$\mu $$ μ BERT and Jumble. MMT even outperforms PIT in its ability to generate such realistic bugs, with similar efficiency per generated mutant. Jumble and $$\mu $$ μ BERT are one or two orders of magnitude slower than MMT and PIT. There are some bugs reconstructed by only one of the tools, including some that only the advanced operators of MMT could replicate. Fifteen percent of the Defects4J project versions had bugs that could not be reconstructed by the mutation operators of any of the investigated tools. This shows that further research in mutation operators, as enabled by MMT, has high potential. Our mutation testing tool MMT is available online https://gitlab.uni-marburg.de/fb12/plt/modbeam-mt/mmt, as well as all the evaluation data (Ancona et al., Evaluation data of comparison of mutation testing tools. https://doi.org/10.5281/zenodo.20054492).

doi.org

SmartCML: a domain-specific modeling language for implementing smart contracts - Software and Systems Modeling

The decentralized and deterministic execution of code, commonly referred to as smart contracts, is one of the most noteworthy capabilities of blockchain technologies, as exemplified by the Ethereum platform. Smart contracts can be utilized in the development of business services, allowing companies to leverage the unique characteristics of this technology, including its capacity for maintaining immutable, transparent, and persistent records on a distributed ledger. However, even those with extensive experience in the field may encounter difficulties in the process of writing smart contracts. To support the development of smart contracts, we propose SmartCML, a domain-specific visual modeling language. The primary objectives of SmartCML are to support of development through visual programming of contract logic on an algorithmic level, to generation of executable code, to facilitate the processing of smart contract models for various tasks, and to serve the communication of information among relevant stakeholders via visual models that serve as documentation and specification aids. The modeling language has been implemented using the ADOxx metamodeling platform. SmartCML models can be transformed into fully functional code for the Ethereum virtual machine. The use of the modeling language is illustrated through two distinct use cases. Moreover, it is demonstrated how SmartCML models can be processed. In addition, the language is qualitatively evaluated through a questionnaire filled by blockchain and modeling experts. The evaluation focuses on the understandability of concepts and the clarity of the notation. The results suggest that the language performs well in these areas. This paper extends previous work with a more detailed description of the language design, implementation, and code generation and an additional modeling procedure as well as the expert evaluation. Further, we explore exemplary model analytics applications.

doi.org

doi.org

Leveraging LLMs to support co-evolution between definitions and instances of textual DSLs: a systematic evaluation - Software and Systems Modeling

Software languages evolve over time for various reasons, such as the addition of new features. When the language’s grammar definition evolves, textual instances that originally conformed to the grammar become outdated. For DSLs in a model-driven engineering context, there exists a plethora of techniques to co-evolve models with the evolving metamodel. However, these techniques are not geared to support DSLs with a textual grammar—applying them to textual language definitions and instances may lead to the loss of information from the original instances, such as layout information and comments, which are valuable for software comprehension and maintenance. This study systematically evaluates the potential of Large Language Model (LLM)-based solutions in achieving grammar and instance co-evolution for textual DSLs. By applying two advanced language models, Claude Sonnet 4.5 and GPT-5.2, and conducting ten experimental runs per case across ten case languages, we evaluate both the correctness of co-evolved instances and the preservation of human-oriented information such as comments and layout. Our results indicate high performance on small-scale cases ( $$\ge $$ ≥ 94% precision and recall for instances with fewer than 20 lines requiring modification), but performance degraded with scale: Claude Sonnet 4.5 maintained 85% recall at 40 lines while GPT-5.2 showed greater sensitivity, failing entirely on the two largest instances. Instance scale also substantially impacts processing efficiency, with Claude’s response time increasing nearly 18-fold for the largest case. In addition, we observe that grammar evolution complexity and deletion granularity impact performance more than change type alone, and prompt transferability across LLMs is limited. These findings identify the conditions under which LLM-based co-evolution succeeds and its scalability limitations, providing practitioners with insights into applicability and researchers with directions for addressing current limitations.

doi.org

Enabling concurrency issue detection for ROS 2 using Timed Petri nets - Software and Systems Modeling

The verification of software applications built on top of the Robot Operating System 2 (ROS 2) is challenging due to the concurrent and physically distributed execution of callback functions. The organization of their execution influences application behavior and performance, because they interact not just with each other, but also with the underlying robotic and system components. Existing approaches lack a full-fledged analysis of the multi-threaded behavior of ROS 2 callbacks and their scheduling. Furthermore, these approaches do not consider the inner structure of callbacks and their organization. In this paper, we improve our model-driven DiNeROS framework using the base of Timed Petri nets (TPN). We integrate these aspects of ROS-based systems and enable the detection of potential defects in ROS applications, such as late, disordered, and deadlocking callbacks within and across nodes. We demonstrate our approach through two case studies involving a mobile industrial robotic arm, showing that the concurrent behavior and interaction of callbacks can be formally described and verified based on Timed Petri nets.

doi.org

2500 years of going meta: from Aristotle to SysML v2 - Software and Systems Modeling

Philosophers have been talking about metaphysics since Aristotle. Logicians have used metalanguages for 80 years. And, in the last 50 years, computer scientists have produced metaobjects, metaclasses and metamodels. We can now create modeling languages able to express their own definitions, allowing tools that can reflect on the very models they are being used to create. What might this mean for the next generation of modeling languages and tools? We are beginning to find out with the Systems Modeling Language version 2 (SysML v2) which is at its core based on reflective metamodeling. This paper summarizes the nearly three millennia of metathinking that has informed the design of SysML v2, and that is now taking us another step down that path into the future.

doi.org

doi.org

Bridging conceptual models and numerical domains: a semantic integration approach for federated co-simulation in MBSE - Software and Systems Modeling

Semantic integration of distributed modeling and simulation services is a major challenge in Model-Based Systems Engineering (MBSE), especially when linking high-level architecture models with detailed numerical simulations. Existing methods often fail to bridge conceptual models and simulation tools, which limits their support for cross-domain co-simulation. In this paper, we present a new approach that combines SysML v2 with ontology-based semantics to create a unified co-simulation platform. A graph database serves as a semantic layer, storing and managing relationships between system architecture elements and simulation artifacts. By federating the Asset Administration Shell (AAS) standard into this knowledge graph, users can query simulation metadata alongside product design information. We also offer an interface to extract component details from SysML v2 repositories in SPARQL-ready form. Our framework enables dynamic configuration and validation of co-simulation scenarios through formal semantic mappings. A representative case study demonstrates how this solution simplifies data integration and enhances traceability in federated engineering environments. These results highlight the potential of semantic technologies to advance simulation-driven MBSE and pave the way for future tool integration and digital engineering infrastructures.

doi.org

Formal verification of fault tolerance mechanisms in multi-layer IoT using Event-B - Software and Systems Modeling

Modern Internet of Things (IoT) systems connect many different parts, from physical devices to cloud-based services, all working together. Keeping these complex systems running reliably, even when problems occur, is a major challenge. A key issue is that a failure starting in one part can quickly spread to others, causing widespread service breakdowns. Current engineering methods often cannot provide solid, mathematically backed promises of fault tolerance, especially in systems built from diverse, spread-out components. This creates a critical need for thorough ways to check and ensure strong resilience at every stage of the IoT system. To meet this need, we introduce a formal verification approach using Event-B. This approach specifically targets important fault-handling strategies like gracefully reducing service, switching to backups, and returning to a safe state after a problem. Our approach begins with abstract, high-level models of how the system should work. We then carefully add more detailed operational information step-by-step through refinement, making sure essential correctness rules are always maintained throughout this process. To thoroughly verify and validate the system, we combine two powerful tools: theorem proving using the Rodin platform to verify logical properties, and model checking using ProB to explore system behavior under different failure conditions. This dual approach allows us to validate both how the system is built and how it acts when things go wrong. The result is a method that delivers strong mathematical guarantees for dependable operation, smooth integration between layers, and consistent recovery actions across the IoT system.

doi.org

Consistency management in model-driven engineering for cyber-physical systems: towards agile design methods - Software and Systems Modeling

Agile methods have shaped the development of enterprise software systems during the last two decades. However, many modern cyber-physical systems (CPS) are still developed in as yet waterfall-like processes. The consequence is that CPS development misses out on such advantages of agile methods as handling changing requirements providing fast updates, or dealing with fast feedback on product quality. This is especially problematic today, when the software in CPS systems is more networked than ever, requiring updates to keep pace in an ever evolving network-connected technical environment, as well as patching too often software-induced cyber-security vulnerabilities. In sum, modern CPS must be developed so as to meet the need for updates at intervals of rapidly accelerating frequency. In this paper, we discuss the lack of systematic cross-model consistency management as one of the reasons why established agile methods are not used in CPS development. We present a road map that leads to systematic consistency management, laying the foundations of novel agile methods in CPS development. We discuss solutions in the context of model-driven automotive systems engineering. This domain especially can serve as a litmus test of agility in CPS development, because automotive systems engineering stands to benefit substantially from agile methods to address such pressing issues as strong assurance of dependability and configurability while also offering the flexibility of software over-the-air updates.

doi.org

A theory of composable modeling language components - Software and Systems Modeling

Modern-day software has become increasingly complex and ubiquitous in many domains. In many cases, the scarcity of software engineering experts means that domain experts must engage in software development tasks. (DSLs) can help bridge this gap by enabling domain experts to express solutions in familiar domain terms. Engineering such (DSLs) is complex. This complexity arises from the variety of artifacts involved—such as grammars, well-formedness rules, and code generators—and from the need to integrate these artifacts across languages. In software language engineering, language workbenches for textual, external modeling languages with translational semantics seem to be a popular, which includes inhabitants such as Xtext, Neverlang, MontiCore, and Spoofax. Yet, reusing existing languages in these environments is often piecemeal and driven by the constraints of specific realization technologies (e.g., Xtend, FreeMarker). This typically requires software language engineers to create DSLs for domain experts, rather than enabling domain experts to reuse and adapt languages themselves. As a result, enabling the systematic reuse of software languages remains a fundamental challenge in software engineering. To reduce the gap between problem domain expertise and software language engineering solution expertise, we have conceived a top-down software language reuse method that enables domain experts to reuse existing languages through formally specified language components that encapsulate the realizations of syntax and semantics of (a fragment of) a language packed ready for systematic reuse. To ease its understanding of our method and its adoption to other technological spaces, we describe our methods and the composition process independent of specific technologies. The presented method of language reuse aims to advance software language engineering for textual, external, translational (DSLs) and may serve as the basis for further investigation of formalizing language reuse.

doi.org

Execution-time opacity control for timed automata - Software and Systems Modeling

Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behaviour. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. In earlier work, it was shown that it can be decided whether a TA is opaque in this setting. In this work, we address control, and investigate whether a TA can be controlled by a strategy at runtime to ensure opacity, by enabling or disabling some controllable actions over time. We first show that, in general, it is undecidable to determine whether such a strategy exists. Second, we show that deciding whether a meta-strategy ensuring opacity exists can be done in EXPSPACE . Such a meta-strategy is a set of strategies allowing an arbitrarily large—yet finite—number of strategy changes per time unit, and with only weak ordering relations between such changes. Our method is constructive, in the sense that we can exhibit such a meta-strategy. We also extend our method to the case of weak opacity, when it is harmless that the attacker deduces that the private location was not visited. Finally, we consider a variant where the attacker cannot have an infinite precision in its observations.

doi.org

Deductive reasoning about embedded systems using reachable abstract states invariants - Software and Systems Modeling

Deductive verification is often more efficient than alternative techniques like model checking at reasoning about functional properties of programs. This is especially true when the program under verification contains very large or unbounded data ranges that model checkers struggle with. However, modular deductive verifiers struggle with verifying global properties, which are often crucial in concurrent and reactive embedded systems. Embedded systems often require complex user-defined invariants to capture the global state for the verification of local annotations, demanding high effort and expertise from the user. In this paper, we propose a method to automatically generate compact invariants that are sufficiently strong to enable effective deductive verification of global properties in embedded systems. Our key idea is that a good level of abstraction can be found automatically by choosing variables for refinement that influence relevant events and process interactions. We use this idea together with abstract interpretation to build a system’s state space, abstracted to the relevant part for a given global property. We demonstrate the effectiveness of our approach on a SystemC design of an automotive control system that has in the past proved challenging to verify.

doi.org

REST in pieces: a controlled experiment to dissect the effects of a domain-specific language for code to cloud API migration - Software and Systems Modeling

Domain-specific languages (DSLs) are an efficient means to counter accidental complexity and are therefore a key technology for model-driven engineering (MDE). Despite the potential of DSLs, there is a lack of empirical research on the practical effects and developer perception of DSL-driven tools. In this paper, we present a controlled experiment with 28 participants around a previously developed DSL- and MDE-based toolchain, which assists the migration of legacy software to REST. We compare the developer performance for (a) “DSL+MDE toolchain" and (b) “classic manual software migration" analysing and quantifying the effects of the DSL, as well as the perception of the DSL by the developers. In certain cases, we measured a significant correlation between toolchain use and performance gains for developers. Detailed analysis of developer activities suggests that the DSL toolchain alleviates tasks which are error-prone or time-consuming in the manual alternative. We then extracted acceptance-hindering factors from the feedback of the participants and derived a series of recommendations for MDE practitioners who seek to develop DSL-based tools.

doi.org

A conceptual framework and city metaphor for investigating the interaction of developers with software artifacts - Software and Systems Modeling

Developers’ interactions with software artifacts during software development activities (e.g., coding, code review) affect their mental states (e.g., cognitive load), which are reflected in biosignals derived from modalities such as eye tracking, electroencephalography, and galvanic skin response. However, existing research lacks an integrated conceptual framework that systematically models the relationship between biosignals and software artifacts in a way that supports both empirical analysis and interpretable visualization of developers’ cognitive aspects when interacting with these artifacts. In this article, to address this gap, we first introduce such a conceptual framework that models the relationship between developers’ biosignals and software artifacts through a systematic linking process. The framework also includes a methodology to seamlessly query and retrieve data across this link. Second, we present a tool prototype that builds upon the framework. Designed for visualizing and navigating large-scale artifacts, its novelty lies in integrating adapted metaphors to generate software city maps that leverage the link to project biomeasures (from biosignals) onto representations of artifacts. Additionally, the tool demonstrates the framework’s applicability to empirical research by bridging conceptualization with practical analysis. This work has key implications for researchers and practitioners in Software Engineering. For researchers, our conceptual framework provides a foundation for studying developers’ interactions with large-scale software artifacts, enabling the investigation of hypotheses on factors influencing complexity, readability, and cognitive load. It also supports visualizing these interactions by projecting biomeasures onto software artifact properties through intuitive city maps. Practitioners can leverage our framework and visualizations to interpret analysis results, identify areas of high cognitive load, and guide task allocation based on the perceived difficulty associated with different artifacts of a software system (e.g., model elements or parts of the code) as reflected in software cities.

doi.org

Reactive synthesis specification review for validity and quality - Software and Systems Modeling

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may not reflect the intended requirements and hence requires validation. Beyond validity, the specification may have quality issues that may impair its readability and maintainability. In this work, we adapt ideas from software engineering and formal verification to present new methods for the validation and the detection of quality issues in reactive system specifications for synthesis. Our first contribution provides a method for specification validation based on a systematic exploration of the specification elements. Specifically, we present algorithms to generate a small scenario suite that demonstrates the meaning of each element in the specification in the context of the behaviors of a controller that is synthesized from it. Our second and third contributions provide means for the detection of quality issues in the specification. Specifically, we present algorithms to detect unnecessary variables that appear in specification elements as well as to detect fine-grained syntactic and semantic specification clones and suggest corresponding refactoring. An important characteristic of our work is that both the algorithms and the controller representation are symbolic. This allows our work to scale well to specifications over large state spaces. We have implemented our ideas in the Spectra synthesis environment and evaluated performance and effectiveness over benchmarks from the literature.

doi.org

Evaluation of modeling methods for systems analysis and development (EMMSAD): past, present, and artificial intelligence eras - Software and Systems Modeling

The evaluation of modeling methods in systems analysis and development (EMMSAD) has been running for about 30 years. EMMSAD started as a platform for systems analysis, design, and development scholars and practitioners to present research works and exchange ideas to advance the fields of systems analysis and design, conceptual modeling, requirements engineering, information systems engineering, and software engineering. After 30 years, it is time to take stock of the advancements, contributions, and current state of the EMMSAD international working conference and to provide research directions for its future evolution. This paper consists of two parts. The first part of the paper examines EMMSAD over the past several decades. The second part of the paper researches the impact of artificial intelligence (AI) on the fields related to and associated with systems analysis and design (SAD). We look at the current trends and future developments of SAD in the era of AI and the rapid advancements of Generative Artificial Intelligence (GenAI), Agentic AI, and research into Artificial General Intelligence (AGI). This paper contributes to understanding the evolution of the EMMSAD, identifying the SAD research trends, and investigating the impact of the rapidly advancing AI on the fields related to and associated with EMMSAD.

doi.org

Engineering a cognition-based specification method - Software and Systems Modeling

Context Software development is inherently a human cognitive task that involves the capture and integration of diverse knowledge and decisions from multiple stakeholders. Existing specification methods and languages mostly rely on computer-based or mathematical primitives, leading to a disconnect between how people naturally think and communicate, and how systems are specified. Therefore, we are investigating a method, called MuDForM (Multi-Domain Formalization Method), to formalize and integrate the knowledge of multiple domains into domain models and into specifications in terms of those domain models. We created a first coherent definition of the method, which emerged from several case study evaluations published in previous works. Goal Establish a method definition that is explicitly based on concepts from human cognition. Method We studied literature in (language) philosophy, linguistics, and cognitive science, to identify concepts that can serve as the cognitive underpinning of the method’s metamodel. We made a model of those concepts and connected them to MuDForM’s metamodel via an explicit method definition structure and analyzed the result. Result The paper defines the conceptual and structural groundwork for illustrating how a specification method can be constructed based on insights into human cognition and communication. It provides a coherent model of cognitive specification aspects, which grounds the modeling concepts in MuDForM ’s metamodel and makes it cognition-based. We also identified additional cognitive aspects that call for future work and the possible extension of the metamodel. The paper clarifies MuDForM ’s objective to support the transformation of natural language into unambiguous, cognition-aligned models.

doi.org

Failure behavior modeling via atomic modeling concepts - Software and Systems Modeling

It is essential to thoroughly analyze the probability of a system failure of safety-critical systems before release. Since this is typically unfeasible through testing alone, probabilistic safety analysis of models is commonly used. However, many modeling languages are lacking in either expressiveness or the ability to reflect the system architecture. The results of these weaknesses are models that are inaccurate in terms of either their behavior or architecture with respect to the system being analyzed. The few languages that overcome both these hurdles are instead overly complicated, resulting in models that are difficult to understand and prone to unintentional errors. To overcome this issue, the modeling language PAFML (Pattern Assisted Failure Modeling Language) is here presented which, while being expressive and able to reflect the system architecture, still satisfies a high level of simplicity. PAFML models are analyzed through transformation to SSF (Stochastic StateFlow), a preexisting language for analysis of stochastic models. PAFML is evaluated both through an interview study with industry professionals in systems safety and through modeling several industrial systems and modeling patterns common in failure behavior models.

doi.org

Formalizing smart contract design patterns with DCR graphs - Software and Systems Modeling

Smart contracts manage blockchain assets and embody business processes. Yet, mainstream languages lack explicit support for process concepts such as roles, action dependencies, and time constraints, leading to increased implementation complexity and analysis challenges. To address this, we use Dynamic Condition Response (DCR) graphs, a formal business process modeling language, to formalize the semantics of smart contract business logic. Modeling smart contracts in DCR graphs involves translating their underlying behavioral logic into a declarative visual model using DCR’s explicit constructs for events, roles, data, time, and inter-event relationships. Furthermore, we systematically model 15 common high-level smart contract design patterns, representing recurring solutions to business logic-level problems. These formalizations reduce ambiguity compared to informal descriptions and serve as language-independent specifications. We demonstrate the modeling process through three complete smart contract case studies that combine six design patterns. Our modeling methodology, formalizations, and correspondence between smart contract semantics and DCR graphs enable future automated analysis and verification.

doi.org

doi.org

Formal modelling and verifying eIDAS multi-factor authentication with interface-based threat analysis - Software and Systems Modeling

This paper introduces a methodology for the formal modelling and verification of multi-factor authentication (MFA) schemes utilized in eIDAS digital identity cards. Our approach employs an interface-based threat model to systematically analyse potential vulnerabilities and enumerate a range of threat scenarios based on varying attacker capabilities. We demonstrate the automated generation of ProVerif models for these scenarios using the Italian Carta di Identità Elettronica (CIE), an eIDAS-compliant digital identity card, as a practical case study. Our analysis reveals several security weaknesses; notably, an attacker possessing only Level 1 (i.e. single-factor) credentials can, in certain circumstances, achieve Level 2 multi-factor authentication without needing to compromise any communication interface. To mitigate these vulnerabilities, we propose minor modifications to the protocols. Furthermore, at Level 3, our analysis shows that the authentication scheme relying on the CieID smartphone application presents a broader attack surface compared to the method employing a PC with a smart card reader. The interface-based modelling and analysis methodology presented in this work offers a valuable framework that can be adapted for the security assessment of other eIDAS digital identity cards.

doi.org

Mu-FRET: a catalogue and tool for requirement refactoring - Software and Systems Modeling

In this paper, we present a catalogue of refactorings for formalised requirements, which improve the structure of requirements without changing their behaviour. As a requirements set evolves and grows in complexity, refactoring is needed to improve clarity, eliminate repetition, and restructure requirements without introducing errors. We integrate our approach with the formal requirement language fretish, and we implement the approach in our Mu-FRET tool. Our approach provides a rigorous grounding for refactoring formalised requirements with guarantees of semantic preservation between requirements before and after refactoring. To this end, Mu-FRET uses the Metric Temporal Logic (MTL) semantics that underpins fretish requirements to formally verify that refactoring has preserved the underlying meaning of the requirements; which is not possible for natural-language requirements. We demonstrate and evaluate our contributions on a range of complex and industry-scale use cases from safety–critical domains including aerospace and medical devices.

doi.org

Integrating SysML and AUTOSAR: model transformation in automotive MBSE - Software and Systems Modeling

Model-Based Systems Engineering (MBSE) is an approach to managing the complexity of modern cyber-physical systems, including automotive systems. In the domain of automotive engineering, it is common for engineers to use a variety of languages at various levels of abstraction, to provide diverse and concrete perspectives of a system. However, a significant incompatibility challenge arises due to weak or nonexistent integration among these languages. This challenge leads to redundant effort and compromised traceability and can hinder the automation of the systems and software development processes. In a previous study, we proposed a model-to-model (M2M) transformation that maps SysML system models into AUTOSAR software models. The transformation considers the client–server and sender–receiver communication patterns supported by AUTOSAR. In this article, we elaborate on the transformation approach in more detail to present a comprehensive account of the transformation, as well as to provide guidelines to practitioners on system design constraints needed to enable the transformation. We also discuss the limitations of the implementation from the perspective of the characteristics of model transformation languages and show how the limitations can be overcome by using a transformation language with different capabilities. We evaluate our transformation approach by applying both implementations to three real-world case studies with different communication patterns and present a comprehensive comparison between the two implementations. Based on our findings, we conclude that the presented model transformation approach is effective in bridging the gap between models at the systems architectural and software architectural levels, and that the previous limitations can be addressed by our new implementation.

doi.org

Model-based digital twin engineering: insights, challenges, and future directions

Software and Systems Modeling - Model-based engineering (MBE) is a powerful paradigm that leverages models as essential pillars of the development process, enabling teams to clarify requirements,...

doi.org