Medical Cyber-Physical Systems (MCPS) play an increasingly critical role in smart healthcare environments. However, the integration of these systems with opaque AI models introduces significant challenges in terms of transparency, traceability, and verifiability. To address these issues, we propose ExMCPS - a model-driven framework that combines ModelBased Systems Engineering (MBSE), Explainable Artificial Intelligence (XAI), and formal modeling techniques to design MCPS that are both explainable and verifiable throughout their lifecycle. We also present a methodological pipeline and an evaluation plan to clarify the applicability of our approach.

Deep Neural Networks (DNN) have recently driven a revolution in various fields of Artificial Intelligence (AI), especially in Deep Learning (DL). However, they remain difficult to design, implement, verify, adapt, and reuse. To address these challenges, this paper introduces DNN-SL, a Domain-Specific Modeling Language (DSML) designed specifically for modeling and verifying DNN architectures. Our approach combines Model-Driven Engineering (MDE) with formal methods to define a multi-layer framework consisting of a DSML definition layer, an MDE implementation layer, and a Maude-based formal semantics layer. This architecture enables DNN models to automatically be translated into formal Maude specifications, thus facilitating the verification of properties including robustness and interpretability. By combining intuitive modeling with formal rigor, our solution simplifies the development of reliable and accessible DL, even for non-experts.

International audience

Systems-of-Systems (SoSs) are increasingly utilized to integrate multiple Constituent-Systems (CSs) and fulfill missions surpassing the capabilities of individual systems. Successful mission execution relies on effective management of time and resources. Time constraints denote the timeframes within these missions must be completed, and resource constraints involve the allocation of necessary resources for execution. Addressing these dynamic behavior factors in SoSs poses significant challenges and necessitates the adoption of control strategies for efficient coordination and execution of missions. To confront these challenges, this paper introduces a novel hybrid approach, merging an MDA technique (TRC-MM: Time-Resource Aware Control Meta-model) and Maude language to formally specify and control missions. This approach specifically incorporates time-resource aware missions, resource dependencies, and control mechanisms in the dedicated TRC-MM. Further, RT-Maude is utilized as the formal specification language to develop an executable formal model for the controller's behavior in SoSs' missions, offering a powerful analysis method to express and verify behavioral properties pertaining to time and resource constraints.

International audience

Elasticity property allows cloud systems to adapt to their input workload by provisioning and deprovisioning resources as the demand grows and drops. However, due to the unpredictable nature of workload, providing accurate action plans to manage a cloud system's elasticity is a particularly challenging task. In this study, the authors propose a bigraphical reactive system‐based approach to provide a formal modelling of cloud systems’ structure using bigraphs , and their elastic behaviours using bigraphical reaction rules . They introduce elasticity strategies to describe cloud systems’ auto‐adaptation behaviours. One step further, they encode the bigraphical specifications into Maude language to enable an autonomic executability of the elastic behaviours and verify their correctness. Finally, they propose a queuing‐based approach to discuss and analyse elasticity strategies in cloud systems through different simulated scenarios.

Today, Design Patterns play a cornerstone role in the development of complex software applications. Although several notations have been proposed to specify them, the kind of formal and tool support they provide is quite limited. In this paper we explore the use of Maude as a formal notation for describing design patterns and reasoning about them. The key to the defined approach is to use a meta model notation, according to MDA approach, and a Maude semantic basis (using the K-framework), for specifying both structural and dynamic aspects of design patterns. In particular, we show how we exploit our combined models approach for reasoning on design pattern inherent operations, such as composition, instantiation, etc.

Context-aware systems are an emerging class of mobile computing systems aiming to provide ubiquitous access to information, communication and computation. These systems are able to sense and adapt automatically to the current environmental context. In this paper, we present a formal approach based on bigraphical reactive systems for modeling the main features of context-aware systems. The proposed formalism provides a clear separation between the part of the system which is affected by the context and the remaining part. In order to illustrate its potential, we apply our approach through a detailed case study of a smart car system.

The use of formal methods is an effective means to improve the reliability and the quality of complex systems. The objective of this work is to adapt one of these methods to UML, so that the systems development depending on this notation can benefit from it. We propose a formal semantic framework, based on rewriting logic, for UML. Thus, we lean on the category model to give precise and sufficient semantics to the various UML diagrams used in system specification. A transcription tool of UML abstract model to Maude object-oriented module is developed. It is able to handle class and sequence diagrams of realistic size.

Petri nets have been used as a formal semantic framework for UML activity diagrams. With UML 2.0 extensions, they become not able to express high level constructions in activity diagrams, namely the traverse-to-completion concept. This one requires a global synchronization between the fork and join nodes which is totally absent in ordinary Petri nets, based on local synchronization. To conserve activities behaviors, we propose zero-safe nets as a richer and more adapted semantic framework for activity diagrams by giving a generic mapping from activities to this Petri nets class. The proposed mapping preserves activities operational semantics while focusing on traverse-to-completion principle as well as synchronization between fork and join nodes and therefore, covering control/data flows and concurrency.

Due to the proliferation of Internet and wireless communication networks, mobility of software components is pervasive in current applications. However, most of the existing Architecture Description Languages (ADLS) lack operators to express mobility primitives. In this paper, we propose a generic rewrite theory for mobility in CBabel, a Declarative Architecture Description Language. Rademaker et al. have associated a rewriting logic semantics to the different constructors of CBabel. We exploit such semantics to extend CBabel with mobility primitives by defining a rewrite theory called mobility-primitives. Our objective is two folds: We propose a rewrite theory for mobility in CBabel. Then, we generalize it to any Architecture Description Language that can be translated to rewriting logic. Such generalization will be obtained by introducing the parameterization notion of Full Maude to the mobility-primitives rewrite theory.

An architectural model for distributed systems description, based on tile logic, has been proposed in a previous work. It is based on dynamic connections between components. A distributed system, in this model, is defined as a set of individual components that are completely free from static interconnection constraints and a dynamic connection is created only if an interaction between two components is needed. Our aim in this paper is to show how a space dimension can be easily added to our architectural model in order to support mobile applications description. A conference reviewing case study is presented to illustrate the benefits of our architectural model.

AADL is an architecture description language based on the MetaH language which describes an embedded system, as a collection of interacting components. The AADL standard associates automata to define dynamic semantics for a thread component. The threads can be in various states such as halted, inactive, or active. An active thread can be waiting for a dispatch, AwaitDispatch state, or computing, Compute state, etc. In this paper, we give a natural semantic model to the thread Compute state, and we associate to the thread component a behavioral annex based on generalized rewriting logic. This allows formal description and analyzing of a thread configuration. Our formalization includes static aspects of thread, and also dynamic ones. The associated models are described by functional and system modules of Maude which is a declarative language based on rewriting logic. Our approach interest is to be able to formally check a large set of properties of AADL threads via analysis tools of Maude environment.

LfP (Language for Prototyping) is an ADL (Architecture Description Language) with a hierarchical and modular structure. In this paper, we propose tile logic (a rewriting logic extension) as a suitable semantic framework for this language. Indeed, it contributes to the formalization of LfP by providing a natural description for concurrency, synchronization and hierarchical composition aspects. A straight consequence of this work is the possibility to describe reconfigurable LfP architectures, and to handle with executable specification in Maude allowing hierarchical formal verification.

The modelling of computing systems using the Multi Agents Systems (MAS) approach nowadays is a method present in the majority of the industry branches: telecommunication, internet, transport, energy, health, etc. So, it is crucial to have rigorous, automatic and effective design and checking methods to ensure these systems development. Our project takes place in the MAS checking scope using the model-checking formal analysis. Although several similar works have been achieved but the absence of a consensus method of formal specification and checking, they all remain incomplete and not general because of the dynamics of this systems type. The main objective of our project is the contribution study of the rewriting logic formalism to the verification of a suitable properties set for the concurrent agents based systems. This work ispractically accomplished with LTL analysis tool of Maude environment.