The advent of digital twins gives us an opportunity to reflect on the relationship between models and modelled systems. We may think of digital twins not merely as models, but as systems for model management, integration, and composition. In fact, digital twins are model-centric systems that maintain a two-way connection between an ecosystem of models and the modelled system, realised through streams of observations and streams of interventions. This connection introduces agility as the digital twin can typically both adapt its models on-the-fly to changes in a modelled system and influence the modelled system’s behaviour. In this paper, we discuss key concepts of digital twins from a formal methods perspective and suggest opportunities and challenges for formal methods in digital twin systems. In particular, we consider how formal techniques can be integral to the digital twin, both in terms of digital twin technology and in terms of digital twin models, as well as notions of correctness for the digital twin itself.

With the advent of AI-driven applications, testing faces new challenges when it comes to the integration of software with AI components. We present a novel testing approach to tackle the integration of software with symbolic AI in the form of knowledge graphs (KG). As the KG is expected to change during the run- and lifetime of the software, we must ensure the robustness of the system w.r.t. changes in the KG. Starting with a single KG, we mutate its content and test the unchanged software with the original test oracle. To address the specific challenges of KGs, we introduce two additional concepts. First, as generic mutations on single triples are too fine-grained to reliably generate a KG describing a different, consistent KG, we introduce domain-specific mutation operators that manipulate subgraphs in a domain-adherent way. Second, we need to specify those parts of the knowledge graph that the software relies on for correctness. We introduce the notion of a robustness mask to describe shapes in the graph to which the mutant must conform. We evaluate our approach on two software applications from the robotic and simulation domain that tightly integrate with their respective KG, as well as three OWL reasoners, where we found several previously unknown bugs.

We introduce a new approach for analyzing distributed hybrid systems based on a generalization of rely-guarantee reasoning. First, we present a system for deductive verification of class invariants and method contracts in object-oriented distributed hybrid systems. In a hybrid setting, the object invariant must not only be the post-condition of a method, but must also has to hold in its post-region. The post-region describes all reachable states after method termination and before another process is guaranteed to be scheduled, and is independent of the dynamics. The system naturally generalizes rely-guarantee reasoning from discrete object-oriented languages to hybrid systems and preserves its modularity to hybrid systems: only one $$d\mathcal{L}$$ -proof obligation is generated per method. The post-region can be approximated using lightweight analyses and we give a general notion of soundness for such analyses. Post-region-based verification is implemented for the Hybrid Active Object language HABS.

Digital twins (DTs) encapsulate the concept of a real-world entity (RE) and corresponding bidirectionally connected virtual one (VE) mimicking certain aspects of the former in order to facilitate various use-cases such as predictive maintenance. DTs typically encompass various models that are often developed by experts from different domains using diverse tools. To maintain consistency among these models and ensure the continued functioning of the system, effective identification of any consistency issues and addressing them whenever necessary is imperative. In this paper, we investigate the concept of consistency management and propose a consistency management framework that addresses various characteristics of DT models. Subsequently, we present three working examples that implement the proposed framework with graph-based techniques. Taking the working examples into account, we demonstrate and argue that our consistency management framework can provide crucial assistance in the consistency management of DT models.

Abstract Self-adaptive systems can be realised as layered systems with a feedback loop: a managing system monitors a managed system, updates an internal model, and adjusts the managed system by means of controllers to maintain given requirements. For example, a digital twin coupled with its physical twin constitute such a self-adaptive system. As the managed system shifts between different stages in its lifecycle, these requirements, as well as the associated analysers and controllers, may need to change. The exact triggers for such shifts in a managed system are often hard to predict: they may be difficult to describe or even unknown. However, the shifts can generally be observed once they have occurred, in terms of changes in the system behaviour. This paper proposes an automated method for self-adaptation in self-adaptive systems to address shifts between lifecycle stages in a managed system. Our method is based on declarative descriptions of lifecycle stages for assets in a managed system and their associated counterparts in the managing system. Declarative lifecycle management provides a high-level, flexible method of self-adaptation for self-adaptive systems to reflect disruptive shifts between stages in a managed system.

Abstract To enable the reuse of Digital Twins, in the form of simulation units or other forms of behavioral models, of single physical components, one must be able to connect and couple them. Current platform and architectures consider mostly monolithic digital twins and offer little support for coupling and checking the consistency of the coupling. The coupling must be internally consistent—satisfy constraints related to their co-simulation—and externally consistent—mirror the structure of the composed physical system. In this paper, we propose an extension to a behavior-extended Digital Twin architecture for individual Digital Twins to include co-simulation scenarios for coupled systems lifted from configuration files, which can be implemented along with a Digital-Twin-as-a-Service platform to make assets reusable in time. To monitor and query these connections, we introduce a semantic lifting service, which interprets the coupled Digital Twins as Knowledge Graphs and enables the use of queries to express internal and external consistency constraints. Two representative case studies for systems with coupled behavior are used for the demonstration of this approach and show that it indeed enables reusability of components and services between different Digital Twins.

With the advent of AI-driven applications, testing faces new challenges when it comes to the integration of software with AI components. We present a novel testing approach to tackle the integration of software with symbolic AI in the form of knowledge graphs (KG). As the KG is expected to change during the run- and lifetime of the software, we must ensure the robustness of the system w.r.t. changes in the KG. Starting with a singular KG, we mutate its content and test the unchanged software with the original test oracle. To address the specific challenges of KGs, we introduce two additional concepts. First, as generic mutations on single triples are too fine-grained to reliably generate a KG describing a different, consistent KG, we employ domain-specific mutation operators, that manipulate subgraphs in a domain-adherent way. Second, we need to specify those parts of the knowledge that the software relies on for correctness. We introduce the notion of a robustness mask as shapes in the graph that the mutant must conform to. We evaluate our approach on two software applications from the robotic and simulation domain that tightly integrate with their respective KG.

Abstract Knowledge bases have been extensively used to represent and reason about static domain knowledge. In this work, we show how to enforce domain knowledge about dynamic processes to guide executions at runtime. To do so, we map the execution trace to a knowledge base and require that this mapped knowledge base is always consistent with the domain knowledge. This means that we treat the consistency with domain knowledge as an invariant of the execution trace. This way, the domain knowledge guides the execution by determining the next possible steps, i.e., by exploring which steps are possible and rejecting those resulting in an inconsistent knowledge base. Using this invariant directly at runtime can be computationally heavy, as it requires to check the consistency of a large logical theory. Thus, we provide a transformation that generates a system which is able to perform the check only on the past events up to now, by evaluating a smaller formula. This transformation is transparent to domain users, who can interact with the transformed system in terms of the domain knowledge, e.g., to query computation results. Furthermore, we discuss different mapping strategies.

A Software Product Line (SPL) is a family of similar programs, called variants, generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs: each variant can depend on variants from other SPLs. MPLs are challenging to model and to implement efficiently, especially when different variants of the same SPL must coexist and interoperate. We address this challenge by introducing the concept of a variability module (VM), a new language construct. A VM constitutes at the same time a module and an SPL of standard (variability-free), possibly interdependent, modules. Generating a variant of a VM triggers the generation of all variants required to satisfy its dependencies. Consequentially, a set of interdependent VMs represents an MPL that can be compiled into a set of standard modules. We illustrate the VM concept with an example from an industrial modeling scenario and formalize it in a core calculus. We define family-based analyses to check that a VM satisfies certain well-formedness conditions and whether all variants can be generated. Finally, we provide an implementation of VM for the Java-like modeling language ABS, and evaluate it with case studies.

We present Crowbar, a deductive verification tool for the Active Object language ABS. Crowbar implements novel specification approaches specifically for distributed systems. For user interaction, counterexamples are presented as executable programs. Crowbar has a modular structure to explore further approaches, and was applied in the largest Active Objects verification study.

ABS is a language for behavioral modeling of distributed, time- and resource-sensitive communicating systems. ABS is based on an executable actor-based semantics with asynchronous method calls, with method call results being delivered via future variables. Data is modeled via a functional, side-effect-free layer of algebraic data types and parametric functions. Actor behavior is expressed in a sequential, imperative way, with explicit suspension points for in-actor cooperative scheduling. A declarative time and resource model allows modeling of time-sensitive actor behavior in a compositional way. A software product line language layer implements model variability via code deltas and feature models. This paper describes the toolchain that makes it possible to simulate ABS models, and lists the most important case studies done with ABS.

We introduce a new system for object-oriented distributed hybrid systems to verify object invariants and method contracts. In a hybrid setting, the object invariant must not only be the post-condition of a method, but also has to hold in the post-region of a method, because the state of the object evolves according to continuous dynamics. The post-region describes all reachable states after method termination before another process runs. This set can be approximated using lightweight analysis of the class structure. The system naturally generalizes rely-guarantee reasoning of discrete object-oriented languages to hybrid systems and carries over its compositionality to hybrid systems: only one dL-proof obligation is generated per method. By reasoning about the minimal size of the post-region, local Zeno behavior can also be analyzed. Our approach is implemented for the Hybrid Active Object language HABS.

Software Product Lines are an established mechanism to describe multiple variants of one software product. Current approaches however, do not offer a mechanism to support the use of multiple variants from one product line in the same application. We experienced the need for such a mechanism in an industry project with German Railways where we do not merely model a highly variable system, but a system with highly variable subsystems. We present the design challenges that arise when software product lines have to support the use of multiple variants in the same application, in particular: How to reference multiple variants, how to manage multiple variants to avoid name clashes, and how to keep multiple variants interoperable.