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.

Formal verification is a promising approach to eliminate bugs at compile time, before they ship. Indeed, our community has verified a wide variety of system software. However, much of this success has required heroic developer effort, relied on bespoke logics for individual domains, or sacrificed expressiveness for powerful proof automation. Building on prior work on Verus, we aim to enable faster, cheaper verification of rich properties for realistic systems. We do so by integrating and optimizing the best choices from prior systems, tuning our design to overcome barriers encountered in those systems, and introducing novel techniques. We evaluate Verus's effectiveness with a wide variety of case-study systems, including distributed systems, an OS page table, a library for NUMA-aware concurrent data structure replication, a crash-safe storage system, and a concurrent memory allocator, together comprising 6.1K lines of implementation and 31K lines of proof. Verus verifies code 3-61x faster and with less effort than the state of the art. Our results suggest that Verus offers a platform for exploring the next frontiers in system-verification research. Because Verus builds on Rust, Verus is also positioned for wider use in production by developers who have already adopted Rust in the pursuit of more robust systems.

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.

Verified systems software has generally had to assume the correctness of the operating system and its provided services (like networking and the file system). Even though there exist verified operating systems and file systems, the specifications for these components do not compose with applications to produce a fully verified high-performance software stack. In this position paper, we lay out our vision for what it would look like to have a verified OS with verified applications, all with good multi-core performance. We've explored a part of the verification by proving a page table correct already, but the larger goal is to lay out a vision for an ambitious project that supports an application verified from its high-level specification down to the hardware.

The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing. We formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.

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.

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.

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

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.

Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data-and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized

The increasing complexity of embedded systems renders software verification more complex, requiring monitoring and formal techniques, like model-checking. However, to use such techniques, system engineers usually need formal expertise to express the software requirements in a formal language. To facilitate the use of model-checking tools by system engineers, our approach uses a UML model interpreter through which the software requirements can directly be expressed in UML as well. Formal requirements are encoded as UML state machines with the transition guards written in a specific observation language, which expresses predicates on the execution of the system model. Each such executable UML specification can model either a Büchi automaton or an observer automaton, and is synchronously composed with the system, to follow its execution during model-checking. Formal verification can continue at runtime for all deterministic observer automata used during offline verification by deploying them on real embedded systems. Our approach has been evaluated on multiple case studies and is illustrated, in this paper, through the user interface model of a cruise-control system. The automata-based verification results are in line with the verification of the equivalent LTL properties. The runtime overhead during monitoring is proportional to the number of monitors.

In order to study the schedulability of complex real-time systems, simulation can be used. Of course, to achieve formal validation of schedulability, simulations must be run long enough such that the schedule repeats. An upper bound on the length of the simulation that is valid for a very wide class of systems running on top of identical multiprocessor platforms is given in a previous work. It is known that this bound is pessimistic. In this paper, we derive a characterization of the exact bound for the same class of systems and describe an algorithm for its computation. We use it to quantify the pessimism of the upper bound on a set of synthesized systems. We also give some directions to explore the complexity vs. tightness trade-off for this problem.

Models have been shown to be useful during virtually all stages of the software lifecycle. They can be reverse engineered from existing artifacts, or created as part of a system's execution, but in many cases models are created by designers from informal specifications. In the latter case, such design models are typically used as means of communication between designers, and developers. They can also in some cases be validated by simulation over test cases, or even by formal verification. However, most existing model simulation or verification approaches require relatively consistent and complete models, whereas design models often start small, incomplete, and inconsistent. Moreover, few design models actually reach the stage where they can be simulated, and even fewer the stage where they can be formally verified. In order to address this issue, we propose a partial modeling approach that makes it possible to animate incomplete and inconsistent models. This approach makes it possible to incrementally improve testable models, and can also help designers reach the stage where their models can be formally verified. A proof-of-concept tool called AnimUML has been created in order to provide means to evaluate the approach on several examples. They are all executable, and some can even undergo model-checking.

To design embedded systems, multiple models of their environments are typically required for different purposes such as simulation, verification, and actual execution. Some of these models abstract the actual physical environment to facilitate Verification and Validation (V&V) activities. Others capture the connection to hardware peripherals, necessary to deploy the systems on actual embedded boards. However, mapping a system to different environment models for different purposes remains a complex task for two main reasons. First, the environment is often tightly coupled with the system, and the board used for its execution. Second, formal properties verified during the design phase must be preserved at runtime. To tackle these issues, we propose an approach for designing UML models in a modular way and deploying them for V&V activities or embedded execution. This approach uses UML modularity mechanisms to specify the system in a generic way, and to connect it to a given (abstract or real) environment. This technique has been applied on several UML models of embedded systems to analyze their behaviors by simulation and LTL model-checking before deploying them on embedded STM32 boards.