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.

In this paper, we provide a new compositional framework for specifying controllability and refinement of service protocols interacting asynchronously. First, we investigate necessary and sufficient conditions for protocols controllability. Then, we give sufficient conditions for preserving controllability of protocols by asynchronous composition. Finally, we propose two protocols refinement relations and show the soundness of our formal framework: independent implement ability of protocols together with the preservation of controllability under protocols by refinement.

Component compatibility and substitutability are widely recognized as the main issues in component- based software engineering (CBSE). Most of existing approaches suffer from the problem of component adaptation. Indeed, components compatibility and substitutability are performed component-to- component without taking into account the context. This paper proposes a new framework where more flexible component protocols compatibility and substitutability relations that depend on the context (environment) can be defined. The proposed approach is based on the notion of component protocol's usability, that is a component such that there exists an environment ensuring the completion and / or the proper termination of the composition of the involved component protocol and that environment. Two optimistic protocols compatibility relations together with two optimistic protocols behavioral subtyping relations related to the principle of substitutability are proposed. Moreover, behavioral refinement of component protocols is studied, and a link between protocols refinement and their usability is established. The soundness of the approach is shown.

In this paper, we present a new and optimistic approach to the definition of component protocols compatibility, and we provide a framework for modeling component protocols together with their composition. This framework is discussed in terms of compatibility and substitutability checks of protocols. According to the optimistic approach, two protocols are compatible if they are composable and their composition leads to a usable protocol, that is a protocol such that there exists an environment ensuring safety and liveness property of the composed protocol, which is obtained by the composition of the involved protocol and that environment. Safety and liveness properties such as deadlock-freeness and proper termination of protocols are considered up to different extents. Based on that, we present two protocols compatibility relations related to the usability concept, together with two behavioural subtyping relations related to the principle of substitutability. We address their soundness by showing the existing link between compatibility and substitutability relations, which have found necessary when dealing with incremental design of protocols.

Component based development (CBD) aims to facilitate the construction of large-scale applications by supporting the composition of simple building blocks into complex applications. Components specification is thus needed to ensure the safety of composing systems from components. This paper focus on component protocols specification and provides a framework for modelling protocols together with their composition. We start by investigating compatibility of component protocols based on service observation. Two compatibility relations together with their characterisation by the preservation to their degree of change property are proposed. Safety and liveness properties such as deadlock-freeness and proper termination of protocols are preserved up to different extents. Then, we propose some behavioural subtyping relations for component protocols related to the principle of substitutability. Finally, we address the soundness of our subtyping relations by showing the existing link between compatibility and substitutability concepts, namely their combination, which have found necessary when dealing with incremental design of components.

The construction of reachability graphs (RG) is one of the most useful techniques to analyse the properties of concurrent systems modelled by Petri nets. Such a graph describes all the possible behaviours of the system, and its construction is straightforward. When high-level Petri nets are under consideration, the size of the graph most often is infinite or large. The reason for this combinatory explosion is twofold: first, the authors have the explosion due to the interleaving of traces which is usual in models of concurrency; the second explosion results from the token identity since each transition occurrence is characterized by the transition and by the tokens involved in this occurrence. Then, the reachability graph of a bounded net may be infinite, if the domains of tokens are infinite. Symbolic reachability graphs (SRG) have been introduced to cope with the latter cause of explosion. By exploiting the symmetries of the net, they are more reduced than the whole reachability graph. This paper introduces a general definition of symbolic reachability graphs. This leads to the introduction of various finite symbolic reachability graphs and to their construction. Two instances of such symbolic reachability graphs are defined. Moreover, a criterion for these two SRG to be finite is given together with computation algorithms.