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.

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.

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.

The increasing complexity of embedded systems renders verification of software programs more complex and may require applying monitoring and formal techniques, like model-checking. However, to use such techniques, system engineers usually need formal experts to express software requirements in a formal language. To facilitate the use of model-checking tools by system engineers, our approach consists of using a UML model interpreter with which the software requirements can directly be expressed as observer automata in UML as well. These observer automata are synchronously composed with the system, and can be used unchanged both for model verification and runtime monitoring. Our approach has been evaluated on the user interface model of a cruise control system. The observer verification results are in line with the verification of equivalent LTL properties. The runtime overhead of the monitoring infrastructure is 6.5%, with only 1.2% memory overhead.

The increasing complexity of embedded systems leads to uncertain behaviors, security flaws, and design mistakes. With model-based engineering, early diagnosis of such issues is made possible by verification tools working on design models. However, three severe drawbacks remain to be fixed. First, transforming design models into executable code creates a semantic gap between models and code. Furthermore, for formal verification, a second transformation (towards a formal language) is generally required, which complicates the diagnosis process. Finally, an equivalence relation between verified formal models and deployed code should be built, proven, and maintained. To tackle these issues, we introduce a UML interpreter that fulfills multiple purposes: simulation, formal verification, and execution on both desktop computer and bare-metal embedded target. Using a single interpreter for all these activities ensures operational semantics consistency. We illustrate our approach on a level crossing example, showing verification of LTL properties on a desktop computer, as well as execution on a stm32 embedded target.

Several approaches, such as the UML MARTE profile or AADL start to reach maturity for the design of Real-Time Embedded System (RTES). The use of such formalisms and their associated verification tools relies on the confidence of the designer in the successful translation of these high- level descriptions into correct executable code. Part of this translation is performed by code generators. However, code generators are often black boxes or difficult to customize. This fact conflicts with the specific needs of the development of RTES where different code generation strategies could be involved. Recently, Model Driven Architecture (MDA) has offered sophisticated tools for model transformation. This paper presents an experimentation: code generation from an AADL model to C code using MDA tools. Based on this experimentation, statements on the interest of MDA tools for this purpose are given. Beyond this feedback, a set of open questions emerged about the need of flexibility of code generators and the different ways for setting this flexibility in MDA tools.