Critical-infrastructure surveillance requires autonomous drone fleets that remain operational after drone losses while maintaining a low communication signature in order to preserve furtivity. This paper presents a system-engineering contribution centered on the loose coupling between Physical Twins (PT) and a Digital Twin (DT). The PT layer is a circulating fleet of homogeneous drones responsible for intrusion detection and for local formation maintenance through a common spacing law based only on neighbor perception, in line with distributed coverage and swarm-control principles. During nominal operation, the DT acts as a trusted suppletive information layer: it provides the operator with a coherent monitoring view of the perimeter while relying on a lazy update policy in which the absence of exception reports is interpreted as nominal operation. Upon receiving exception reports, the DT switches to a predictive mode in which it aggregates information into mission-level knowledge, estimates the current weakening of perimeter protection from infrastructure degradation, and evaluates whether local recovery remains sufficient. The DT does not aim at exact replication of the fleet state; it reasons from bounded approximations whose associated confidence conditions whether reinforcement should be triggered before the estimated weakness reaches a breach threshold. Representative scenarios illustrate rapid loss absorption, slower spare assimilation, and the broader distinction between resilience and antifragility.

Live modeling is the ability to change an executable model at runtime, and without having to restart its execution. Sometimes this 'breaks' the ongoing execution, but in many cases, it does not have to. In earlier work, we reduced this problem to detecting fine-grained read/write conflicts between the recorded history of edit operations (created by the user) and execution steps (created by the interpreter). In this paper, we extend our approach by adding the ability to perform model checking during live modeling sessions. We motivate that this further enhances the live modeling experience, producing counter-examples or 'witness traces' relative to the current execution state, as a possible 'future', integrated with the execution and edit history, minimizing the mental gap. The model checker itself is generic, and uses (via an adapter) the language's existing interpreter. This way, we could implement this paper's running example in a working prototype with relatively little effort.

Model-Based Systems Engineering (MBSE) has made substantial progress in managing system complexity, yet it still lacks principled support for understanding system behavior during early design. SysML v2 introduces a richer semantics for modeling behavior, but its utility remains limited by a lack of executable semantics, weak interoperability, and the absence of native support for formal verification and design-space exploration. We argue that a paradigm shift is needed, one in which behavioral models become first-class, executable artifacts, navigable within a dynamic design multiverse. This position paper presents the vision for the Living SysML v2 Blueprint, a next-generation SysML v2 virtual machine that unifies dynamic execution, multiverse exploration, and native formal verification. Central to this vision is the Transparent Execution, Observation, and Control (TEOC) API, enabling accurate semantic inspection and tool interoperability without model transformation. By tolerating incomplete models and exposing structured execution traces, the LivingBlueprint VM empowers system engineers, verification experts, and business strategists to engage with design decisions iteratively, rigorously, and early. This architecture redefines the semantics–verification–execution triad at the heart of MBSE, offering new foundations for explainability, trust, and AI-augmented design. This paper outlines the theoretical pillars, practical challenges, and community-wide opportunities of this approach and invites collaborative efforts toward a new class of MBSE platforms centered around behavioral fidelity and multiverse awareness.

Real-world design processes often involve the evolution and divergence of design paths (by branching, revising, merging, etc.), especially when multiple stakeholders or teams operate concurrently and/or explore different alternatives for complex and heterogeneous systems. Unfortunately, this variability in time and space can not be directly managed in current modeling spaces but requires resorting to external tools and methodologies. In order to tackle this problem, we introduce the Design Multiverse. The Design Multiverse aims to integrate in the modeling space a selection of revisions and variants, representing snapshots of a design state composed of multiple artifacts. This enables stakeholders to seamlessly trace, analyze, and manage design decisions, system variants, and their interdependencies. Concretely, in this paper we present a conceptual definition of the Design Multiverse, discuss usage scenarios such as model product lines and model/metamodel co-evolution, and propose an implementation leveraging the model federation paradigm.

Each software modeling tool typically supports only a few tasks among model creation, simulation, debugging, analysis, transformation, deployment, and monitoring. Therefore, multiple tools must generally be jointly used. However, few guarantees are generally provided regarding their semantic compatibility. This paper presents AnimUML, a UML modeling tool supporting most modeling tasks, and helping users from early model creation to deployment. Semantic compatibility between tasks is ensured by leveraging a single semantics implementation. AnimUML is successfully used as a framework on which to build research activities. It is also used to teach embedded UML modeling, as well as UML model verification.

Live modeling is the ability to edit an executable model at run-time, and to subsequently continue the execution instead of having to restart it. Few modeling frameworks support this feature. Much of the research concerning live modeling attempts to bring “liveness” to existing modeling languages and environments, which is a complex, and often ad hoc endeavor. We instead argue to build modeling environments on an operation-based versioning foundation, to not only record edit operations, but also execution steps on an explicit run-time model. This reduces the complexity of patching the run-time state with edit operations to a simple merge-operation, while getting powerful features such as collaborative editing and debugging “for free.”

In this paper, we present experience feedback on the use of animation and debugging tools to build, improve, and verify a UML model of the Paxos consensus algorithm. The need for consensus appears in our IoT industrial context, where we need to switch between several service providers for message passing, depending on their availability and quality of service. However, Paxos is notoriously difficult to understand, and as we plan to expand on the original idea to adapt it to our needs, we have to make sure that the base model is correct as well as fully understood by the developers. To this end, we developed an AnimUML model of Paxos, making it interactive and thus easier to work with. During its construction, we tried to understand how to verify that our requirements are met. By replicating existing scenarios step by step, we found that our model was incomplete. To validate how further model modifications changed this, we wanted to write breakpoints to reach these specific situations, but we found that configuration-based breakpoints were not sufficient in this regard. This led us to leverage the possibilities offered by a temporal multiverse debugger, allowing the creation of temporal breakpoints breaking on scenarios described by different languages of temporal logic. With these tools, we can not only correct the model faster, but also prove that some scenarios are possible or not, allowing for a first step in the model formal verification while keeping it accessible to non-experts of the domain.

Multiverse debugging extends classical and omniscient debugging to allow the exhaustive exploration of non-deterministic and concurrent systems during debug sessions. The introduction of user-defined reductions significantly improves the scalability of the approach. However, the literature fails to recognize the importance of using more expressive logics, besides local-state predicates, to express breakpoints. In this article, we address this problem by introducing temporal breakpoints for multiverse debugging. Temporal breakpoints greatly enhance the expressivity of conditional breakpoints, allowing users to reason about the past and future of computations in the multiverse. Moreover, we show that it is relatively straightforward to extend a language-agnostic multiverse debugger semantics with temporal breakpoints, while preserving its generality. To show the elegance and practicability of our approach, we have implemented a multiverse debugger for the AnimUML modeling environment that supports 3 different temporal breakpoint formalisms: regular-expressions, statecharts, and statechart-based Büchi automata.

In the world of executable modelling languages, live modelling is a feature of integrated modelling, execution/simulation and debugging environments, where the user can alter the models during execution. This reduces the need to compile and restart the execution after making a change to the model. In this paper, we point out a number of desirable features for “next generation” live modelling, simulation and debugging. Most importantly, we would like to transpose collaborative features (such as: (a) synchronous collaboration, branching and merging) that are already part of some modelling/editing environments, onto execution and debugging environments. We also point out the issue of doing all of this in a compositional manner, in order not to repeat the tooling development effort for every new language that we want to support. As a solution, we propose using a language-agnostic versioning system for graphs, that tracks changes to both the design-time models and their run-time configurations, in a unified manner.

Security by Design (SbD) has gained increasing interest over the past decade. While iterative processes and legacy preservation aim to reduce costs and mitigate risks through continuity, SbD encourages a break in the way we do things with a simple idea: dealing with new threats, leading to new risks, requires a complete rethink of our design processes. In embedded systems, security has been more or less left aside for a long time, with performance being the main objective. When security concerns emerged, the response was to adapt existing solutions with security patches. This is neither sustainable (to change from simple embedded systems to complex systems-on-chip) nor simply effective. It is necessary to change the mindset, which will lead to new practices. But the central question is: "How can we put security at the heart of the design process?" The aim of this paper is to contribute to this reflection by providing a rapid prototyping environment (modeling and simulation-based systems engineering) for the hardware mechanisms responsible for the deployment of rights management services.

Giving accurate and relevant static analysis feedback to modeling tool users significantly helps them design useful models. This feedback is even more valuable when it comes with completion proposals, called quick fixes, which users can apply to automatically resolve specific issues. However, implementing such static analysis and quick fix tooling is tedious and error prone. For instance, providing accurate messages typically requires decomposing complex model queries into simpler ones, while suitably handling their dependencies. Moreover, each quick fix should actually resolve the issue it is supposed to fix, which is not always easy to ensure. This paper presents an approach that leverages reverse propagation of OCL-like boolean expressions to provide correct-by-construction quick fixes. It only requires adding specific annotations to expressions in order to guide quick fix computation. A proof-of-concept implementation of this approach on the AnimUML partial modeling tool is described. It is able to automatically construct messages, to report different messages depending on which part of a predicate fails, and to provide quick fixes.

Multiverse debugging is an extension of classical debugging methods, particularly adapted to non-deterministic systems. Recently, a language-independent formalization was proposed. Moreover, multiverse debugging is particularly beneficial for specification and design languages, such as UML. However, this method suffers from scalability issues during breakpoint lookup. This problem arises due to the exhaustive exploration performed on the potentially infinite state-space of the system. In this paper, we tackle this problem by introducing Reduced Multiverse Debugging, an extension proposing a way for the user to define reduction policies used during breakpoint lookup. We enrich the formalization of multiverse debugging with a modular breakpoint lookup strategy, which allows the integration of the reduction policy. We validate our approach by implementing a practical UML Statechart debugger in the AnimUML web framework. We show several ways the reduction can be applied, using methods such as predicate abstraction for breakpoint lookup on an infinite state-space, removing irrelevant variables, or creating classes of equivalent values. Moreover, we show the possibility to integrate probabilistic reduction strategies. Relying on hash collisions, these strategies can be iteratively refined to increase precision.

To ensure correctness of critical systems, swarm verification produces proofs of failure on systems too large to be verified using model-checking. Recent research efforts exploit both intrinsic parallelism and low-latency on-chip memory offered by FPGAs to achieve 3 orders of magnitude speedups over software. However, these approaches are limited to safety verification that encodes only what the system should not do. Liveness properties express what the system should do, and are widely used in the verification of operating systems, distributed systems, and communication protocols. Both safety and liveness properties are of paramount importance to ensure systems correctness. This paper presents Dolmen, the first FPGA implementation of a swarm verification engine that supports both safety and liveness properties. Dolmen features a deeply pipelined verification core, along with a scalable architecture to allow high-frequency synthesis on large FPGAs. Our experimental results, on a Xilinx Virtex Ultrascale+ FPGA, show that the Dolmen architecture can achieve up to 4 orders of magnitude speedups compared to software model-checking.

Model verification techniques, such as model checking, generally require relatively advanced expertise. They are therefore typically used in applications where their usefulness is especially appreciated, if not necessary, and can offset their costs. Critical system design has, for instance, been one of the main consumers of such techniques. They could however bring benefits to many other domains. Development times can be shortened by the drastically reduced number of mistakes in verified design models. Moreover, they can help reduce the number of bugs remaining in shipped products. Lowering barriers to entry for the application of these techniques should therefore have a significant impact. In this work, we show how model checking can be applied to UML models in the smart home context. The models were created with AnimUML, which makes them markedly easier to create than with traditional tools. Furthermore, this tool’s direct model analysis support at the UML level makes it relatively simple to verify properties. It was able to detect several corner case issues, which would have been much harder to detect, and especially diagnose, with testing only. Besides being time consuming, testing reaches its fundamental limits, checking what the system should not do. Besides, in the home automation context, the problem is even more complex due to the distributed nature of the problem [1]. The situation can certainly be improved by using formal verification approaches, like model-checking. These techniques, naturally geared towards distributed systems, allow the verification of properties expressing what the system should do, which naturally completes the correctness specification of a system. During the last decade, tremendous progress was achieved on this axis [2, 3], however most of the proposed approaches and tools require a high-degree of sophistication from the home automation designer. Moreover, the marketing target of home automation solutions, like Google Smart Home1, is wide and targets non-expert users. Nevertheless, the modeling community started a push towards lively verification environments [4], which enables seamless user interaction during the design and debugging process. The AnimUML environment [5, 6, 7] pushes the frontiers of this approach by allowing not only early debugging of high-level specifications, but also

The mapping of software verification algorithms on FPGA promise orders of magnitude faster verification. FPGASwarm shows 900X speedup over software swarm verification. However, this approach misses important optimization opportunities and glosses over algorithmic design-space exploration. This paper introduces Carnac, a deeply pipelined swarm verification architecture, which by exposing the algorithmic variability points can realize multiple verification algorithms. Furthermore, we introduce the Mixed Young Random Frontier-Bounded (MYR_FB), a new swarm verification algorithm, found through an efficiency-based design-space exploration. Evaluated on the BEEM benchmark, the MYR_FB algorithm shows up to 144% efficiency gain over FPGASwarm on 72% of the models. The Carnac architecture runs at 400MHz on Xilinx Ultrascale+ FPGA, and can accommodate twice more verification cores than FPGASwarm. Overall the evaluation shows a 7.58X speedup over FPGASwarm, while enabling an unprecedented scalability on high-end FPGAs.

Practice with feedback is essential to most learning activities. Although invaluable, an instructor's availability to give feedback is necessarily time-limited, but can sometimes be complemented by automated feedback. This is actually the case when learning a new programming language: students can get automated low-level feedback on their production from compilers, interpreters, and program output. However, this is generally not possible when learning a modeling language. Even for UML, which has multiple available execution engines, getting automated feedback from a model's execution requires it to be virtually as precise and complete as a program. In previous work, we presented AnimUML, which makes it possible to animate incomplete and inconsistent models. The work presented here shows how AnimUML works in practice, and how it can be used when teaching modeling. With it, students can observe the behavior or existing models, thus getting a first hands-on experience with the UML semantics. They can then start creating and animating their own models, all along getting a similar level of automated feedback as when learning a programming language. Finally, because it can be connected to a model checker, AnimUML can also help teach model verification.