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.

This paper presents experience feedback on how we managed to formally verify properties on semi-formal models of a Life Cycle Management System (LCMS) for smart devices. These devices are typically structured around a System on Chip (SoC), which can provide built-in hardware security. They can offer the possibility to make the deployment of Product-Service Systems (PSSs) to consumers easier, through traceability and collaborative consumption rule enforcement. A PSS is a business model in which products and services are tightly connected. One of the main advantages of such a PSS is that it optimizes product use, with a positive environmental impact. Associating the LCMS with a blockchain-based protocol makes it possible to avoid centralization. Semi-formal UML models of such a LCMS, as well as the informal properties it must comply with, were defined in order to explore its design space and evaluate the outcomes of specific design choices. However, the security of the LCMS implementation must be guaranteed, including protocols and architecture. For that purpose, these models and properties were later improved to be formally verifiable, which ensures the security of their implementation at the expense of added complexity. The verification was carried out using two available software tools: VerifPal for the protocol model, and AnimUML (developed by one of the authors) for the architecture model. This makes the procedure accessible for non-specialists in formal verification. Finally, our feedback on the whole process as well as on VerifPal is also provided.

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.

Abstract To cope with the increased complexity of systems, models are used to capture what is considered the essence of a system. Such models are typically represented as a graph, which is queried to gain insight into the modelled system. Often, the results of these queries need to be adjusted according to updated requirements and are therefore a subject of maintenance activities. It is thus necessary to support writing model queries with adequate languages. However, in order to stay meaningful, the analysis results need to be refreshed as soon as the underlying models change. Therefore, a good execution speed is mandatory in order to cope with frequent model changes. In this paper, we propose a benchmark to assess model query technologies in the presence of model change sequences in the domain of social media. We present solutions to this benchmark in a variety of 11 different tools and compare them with respect to explicitness of incrementalization, asymptotic complexity and performance.

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.

Industrial use of Model Driven Engineering techniques has emphasized the need for efficiently store, access, and transform very large models. While scalable persistence frameworks, typically based on some kind of NoSQL database, have been proposed to solve the model storage issue, the same level of performance improvement has not been achieved for the model transformation problem. Existing model transformation tools (such as the well-known ATL) often require the input models to be loaded in memory prior to the start of the transformation and are not optimized to benefit from lazy-loading mechanisms, mainly due to their dependency on current low-level APIs offered by the most popular modeling frameworks nowadays. In this paper we present Gremlin-ATL, a scalable and efficient model-to-model transformation framework that translates ATL transformations into Gremlin, a query language supported by several NoSQL databases. With Gremlin-ATL, the transformation is computed within the database itself, bypassing the modeling framework limitations and improving its performance both in terms of execution time and memory consumption. Tool support is available online.

Some areas in computer science are characterized by a shared base structure for data artifacts (e.g., list, table, tree, graph, model), and dedicated languages for transforming this structure. We observe that in several of these languages it is possible to identify a clear correspondence between some elements in the transformation code and the output they generate. Conversely given an element in an output artifact it is often possible to immediately trace the transformation parts that are responsible for its creation. In this paper we formalize this intuitive concept by defining a property that characterizes several transformation languages in different domains. We name this property additivity: for a given fixed input, the addition or removal of program elements results in a corresponding addition or removal of parts of the output. We provide a formal definition for additivity and argue that additivity enhances modularity and incrementality of transformation engineering activities, by enumerating a set of tasks that this property enables or facilitates. Then we describe how it is instantiated in some well-known transformation languages. We expect that the development of new formal results on languages with additivity will benefit from our definitions.

Within a given modeling platform, modeling tools interoperate efficiently. They are generally written in the same general purpose language, and use a single modeling framework (i.e., an API to access models). However, interoperability between tools from different modeling platforms is much more problematic. In this paper, we argue that fUML may be leveraged to address this issue by providing a common execution language, and by abstracting modeling frameworks into generic actions that perform elementary operations on models. Not only can user models benefit from a unified execution semantics, but modeling tools can too.

International audience

Different formal methods have presented plenty of formal models for system specification and proof. Hence the problem of bridging these formal models rises. MDE is a new paradigm in software engineering, which implements software by (meta-)modeling and model transforming. In this paper, we provide a MDE based approach for bridging heterogeneous formal models: Firstly, the heterogeneous formal models are introduced into MDE as domain specific languages by metamodeling. Then, transformation rules are built for semantics mapping. At last, model-text syntax rules are developed, so as to map models to programs. Our approach could be applied on formal models in both graphical style and grammatical style. A case study of bridging MARTE to LOTOS is also illustrated showing the validity and practicability of our approach.

Model differentiation techniques, which provide the capability to identify mappings and differences between models, are essential to many model development and management practices. There has been initial research toward model differentiation applied to Unified Modeling Language (UML) diagrams, but differentiation of domain-specific models has not been explored deeply in the modeling community. Traditional modeling practice using the UML relies on a single fixed general-purpose language (i.e., all UML diagrams conform to a single metamodel). In contrast, Domain-Specific Modeling (DSM) is an emerging model-driven paradigm in which multiple metamodels are used to define various modeling languages that represent the key concepts and abstractions for particular domains. Therefore, domain-specific models may conform to various metamodels, which requires model differentiation algorithms be metamodel-independent and able to apply to multiple domain-specific modeling languages. This paper presents metamodel-independent algorithms and associated tools for detecting mappings and differences between domain-specific models, with facilities for graphical visualization of the detected differences.

Domain modeling promotes the description of various facets of information systems by a coordinated set of domain-specific languages (DSL). Some of them have visual/graphical and other may have textual concrete syntaxes. Model Driven Engineering (MDE) helps defining the concepts and relations of the domain by the way of metamodel elements. For visual languages, it is necessary to establish links between these concepts and relations on one side and visual symbols on the other side. Similarly, with textual languages it is necessary to establish links between metamodel elements and syntactic structures of the textual DSL. To successfully apply MDE in a wide range of domains we need tools for fast implementation of the expected growing number of DSLs. Regarding the textual syntax of DSLs, we believe that most current proposals for bridging the world of models (MDE) and the world of grammars (Grammarware) are not completely adapted to this need. We propose a generative solution based on a DSL called TCS (Textual Concrete Syntax). Specifications expressed in TCS are used to automatically generate tools for model-to-text and text-to-model transformations. The proposed approach is illustrated by a case study in the definition of a telephony language.

We take here a broad view of model engineering as encompassing different approaches such as the OMG MDA/spl trade/ proposal as stated in R. Soley (2000), the Microsoft Software Factories view based in J. Greenfield (2004), and many others. We distinguish the three levels of principles, standards and tools to facilitate the discussion. We proposed the idea that there exist a common set of principles that could be mapped to different implementation contexts through the help of common standards. We illustrate our claim with AMMA, a lightweight architectural style for a model-engineering platform that is currently mapped onto the eclipse modeling framework according to F. Budinsky et al. (2004).