Low-cost Internet of Things (IoT) weather stations enhance spatial and temporal coverage for hyperlocal forecasting, especially in remote or hard-to-reach areas where traditional monitoring infrastructure is limited. However, their dependable operation is affected by component reliability, message delivery performance, and energy-related constraints, particularly battery depletion and solar recharge variability. This paper presents a dependability analysis of a real IoT-enabled weather monitoring platform based on a Weather Monitoring Approach (WMA), modeled using Stochastic Petri Nets (SPNs) to evaluate availability and reliability, while explicitly modeling energy autonomy as a cross-cutting operational constraint that affects continuous operation. Results show that the proposed WMA significantly increases operational availability, reduces failure probability, and improves energy autonomy by reducing the likelihood of battery depletion and extending operational continuity. In addition, the optimized communication configuration substantially decreased the latency required for near-certain message delivery, highlighting the impact of transmission tuning on system dependability. The proposed WMA provides a means to analyze configuration and design changes that can further improve system dependability, demonstrating how the combination of reliability modeling, energy autonomy mechanisms, and efficient communication strategies can substantially enhance the dependability of IoT-enabled weather monitoring systems and support continuous operation in regions with limited maintenance accessibility.
Developers spend a large portion of their time on software comprehension, making it essential to understand how different artifacts – models and code – support this activity. While prior research has primarily explored the use of models as complementary aids for understanding code, limited evidence exists regarding their standalone effectiveness in conveying software’s structural and behavioral aspects. This gap is particularly relevant in contexts such as Model-Driven Engineering (MDE) and Low-Code/No-Code (LCNC) approaches, where models often serve as the primary or sole representation of software. The paper reports on two complementary controlled experiments that investigate how models and code contribute to understanding software structure and behavior. The first experiment compares comprehension when only reverse-engineered UML models or source code were available (code-centric settings), mimicking scenarios in agile or AI-assisted development where models are outdated or absent. The second experiment focuses on model-driven settings, examining whether providing generated code alongside platform-independent models improves comprehension and whether differences in code generators influence performance. The results demonstrate that models and code achieve comparable overall correctness, and thus models alone may be sufficient in model-centric scenarios where access to code is limited or unavailable. The experiments also reveal a consistent structure-behavior comprehension gap, show differences in comprehension across tasks regardless of artifact type, and indicate that adding code to models can both clarify and confuse comprehension depending on context.
Enterprise modeling (EM) typically includes multiple perspectives to analyze or design an organization, which is supposed to reduce the complexity of the modeling process and improve the structure of the resulting enterprise models. However, for non-modeling experts, i.e., stakeholders without solid training in EM, the development and integration of different model perspectives remains a challenge. Based on previous research in conceptual modeling, the paper investigates the use of large language models (LLMs) to support non-modeling experts of multi-perspective EM. Positioned in the roadmap for increasing the reach of EM, an LLM-based toolchain and reusable prompts for generating multi-perspective enterprise models from textual descriptions are proposed and evaluated. The results indicate that LLMs can be seen as assistive technology for certain tasks in EM. The main contributions of the paper are (1) an analysis of the state of research in LLM use in EM, (2) a study on LLM use for producing multi-perspective enterprise models, and (3) positioning LLMs in the roadmap for increasing the reach of EM.
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.
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 μ BERT. Our evaluation shows that MMT and PIT are significantly more effective and efficient than μ BERT and Jumble. MMT even outperforms PIT in its ability to generate such realistic bugs, with similar efficiency per generated mutant. Jumble and μ 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).
Runtime verification of temporal properties is essential for ensuring the correctness and reliability of real-time systems, particularly in cyber-physical systems. A significant challenge in this domain is the effective prediction of property failure or success, especially when dealing with partially observable systems. This paper addresses these challenges by developing an Assumption-Based Runtime Verification (ABRV) approach for a continuous real-time setting. Our method exploits assumptions about the system’s behavior, specified as Timed Automata, to enable monitors to predict future outcomes and handle unobservable system parts, such as internal faults. Properties to be monitored are specified using Metric Interval Temporal Logic (MITL). The approach also includes formalizing observations with data and time uncertainty using sequences of timed constraints. We present a zone-based online algorithm for computing the monitoring verdict, implemented on top of the UPPAAL tool. Experimental evaluation on proof-of-concept cases demonstrates the approach’s feasibility and effectiveness, illustrating how assumptions facilitate earlier verdicts, enable monitoring of properties dependent on unobservable events, and provide insights into scalability.
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.
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.
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.
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.
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.
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.
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.
This guest editorial presents the special section of the first iteration of the Engineering Digital Twins conference (EDTconf 2024). The best papers from EDTconf 2024 were invited to be revised and significantly expanded. Finally, five papers were accepted for publication in the special section. These papers represent different aspects regarding the engineering and application of digital twins, including the use of AI, life-cycle management, and the use of digital twins for DevOps.
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.
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.
