Guaranteeing cyber-physical systems (CPSs) correct and proper behaviour is an essential and challenging issue, as they are widely used in many application domains. This paper aims to contribute to the flexible design and development of structured CPSs, composed of similar elements and capable of (self-)adaptation to satisfy evolving internal and external constraints, e.g. using control theory. To this end, based on a model of a hierarchical motif for modeling both systems’ elements and controllers, we introduce a control-compatible notion of a motif refinement, and then we show that the stability of control can be preserved regarding a refinement-based development. Motivations and contributions are illustrated by the smart building example.

When designing new web applications, developers must cope with different kinds of constraints relative to the resources they rely on: software, hardware, network, online micro-services, or any combination of the mentioned entities. Together, these entities form a complex system of communicating interdependent processes, physical or logical. It is very desirable that such system ensures its robustness to provide a good quality of service. In this paper we introduce Chips, a language that aims at facilitating the design of models made of various entwined components. It allows the description of applications in the form of functional blocks. Chips mixes notions from control theory and general purpose programming languages to generate robust component-based models. This paper presents how to use Chips to systematically design, model and analyse a complex system project, using a variation of the Adaptable TeaStore application as running example.

The sheer complexity of modern systems requires compositional approaches to variability modelling. To manage the variability of large systems’ architecture, feature models are widely used at design-time, with several operators defined to allow their composition. However, complex systems’ architectures may evolve at run-time by acquiring new features and functionalities while respecting new constraints. To address this challenge, this paper defines composition operators for component-based run-time variability models that not only encode these feature model composition operators, but also ensure safe run-time reconfiguration. To prove the correctness and compositionality properties, we propose a novel multi-step 𝒰𝒫 -bisimulation equivalence and use it to show that the component-based run-time variability models preserve the semantics of the composed feature models. In addition, reachability results permit safe reconfiguration.

Self-adaptation of complex systems is a very active domain of research with numerous application domains. Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies, which describe needs for reconfiguration. In this context, an adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their utility. The adaptation policy has to be faithfully implemented by the system, especially w.r.t. the utility occurring in the rules, which are generally specified for optimizing some extrafunctional properties (e.g. minimizing resource consumption). In order to validate adaptive systems’ behavior, this paper presents a model-based testing approach, which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. As a result, the relative frequencies of the reconfigurations can be measured in order to determine whether the adaptation policy is faithfully implemented. To illustrate the approach the paper reports on experiments on the case study of platoons of autonomous vehicles.

Cloud applications and cyber-physical systems are becoming increasingly complex, requiring frequent reconfiguration to adapt to changing needs and requirements. Existing approaches compute new valid configurations either at design time, at runtime, or both. However, these approaches can lead to significant computational or validation overheads for each reconfiguration step. We propose a component-based approach that avoids computational and validation overheads using a representation of the set of valid configurations as a variability model. More precisely, our approach leverages feature models to automatically generate, in a component-based formalism called JavaBIP, run-time variability models that respect the feature model constraints. Produced run-time variability models enable control over application reconfiguration by executing reconfiguration requests in such a manner as to ensure the (partial) validity of all reachable configurations. We evaluate our approach on a simple web application deployed on the Heroku cloud platform. Experimental results show that the overheads induced by generated run-time models on systems involving up to 300 features are negligible, demonstrating the practical interest of our approach.

In the context of component-based systems, this paper presents the automated generation of initial states, from which an adaptive system starts to receive sequences of events that aim to provoke reconfigurations. For generating these states, also called configurations, we present a combinatorial algorithm supporting various architectural elements and relationships among them, while satisfying consistency constraints expressed by invariants. Moreover, this algorithm deals with the system-dependant instantiations of the primitive and composite components, parameters and relations, in order to produce meaningful structured configurations. While testing adaptation policies for componentbased systems, this algorithm allows us to improve the capability of fulfilling coverage criteria by using different initial configurations. To illustrate the approach, the paper reports on experiments on a simulation with platoons of autonomous vehicles.

Self-adaptive systems have to implement adaptation policies described by sets of rules that express how the components are reconfigured within the system, the priority of a given reconfiguration to happen, when a given (sequence of) event(s) occurs, and when specific conditions on the system state are satisfied. However, when this priority is given by a fuzzy value (e.g., high, medium, low) depending on external and internal events, it has to be implemented inside the software with particular implementation choices made. This paper is dedicated to the validation of adaptation policies, using a model-based testing approach and a verdict establishment that is based on both the runtime verification of temporal properties, and the detection of inconsistencies between the adaptation policy and the reconfigurations implemented in the self-adaptive system. We propose means to establish a test verdict based on the respect of the adaptation policy by the implementation, along with coverage measures of the rules. This provides interesting feedback on the adaptation policy rules, allowing to detect reconfigurations that should not have occurred, high-priority reconfigurations that are never triggered, or low-priority reconfigurations that are too frequently executed, potential inconsistencies in the rules, or wrong interpretation of priorities. The test verdict is made based on the analysis of the execution traces of the system, which is stimulated using a usage model that describes the probabilities of external events to occur. An experiment, performed on a vehicular ad-hoc network of autonomous vehicles, illustrates the interest of the approach.

System modeling is a classical approach to ensure their reliability since it is suitable both for a formal verification and for software testing techniques. In the context of model-based testing an approach combining random testing and coverage based testing has been recently introduced [9]. However, this approach is not tractable on quite large models. In this paper we show how to use statistical approximations to make the approach work on larger models. Experimental results, on models of communicating protocols, are provided; they are very promising, both for the computation time and for the quality of the generated test suites.

In event systems, contrarily to sequential ones, the control flow is implicit. Consequently, their abstraction may give rise to disconnected and unreachable paths. This paper presents an algorithmic method for computing a reachable and connected under-approximation of the abstraction of a system specified as an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicate-based abstraction. To be of interest, these concrete transitions have to be reachable and connected to each other. We propose an algorithmic method that instantiates each of the abstract transitions, with heuristics to favour their connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.

Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. When abstracting still a test has to be a concrete connected and reachable event sequence. This paper presents a test generation method based on computing a reachable and connected under-approximation of the abstraction of an event system. We compute the under-approximation with concrete instances of the abstract transitions, that cover all the states and transitions of the predicatebased abstraction. We propose an algorithmic method that instantiates each of the abstract transitions, and maintains for widening it a frontier of concretely reached states. We present heuristics to favour the instances connectivity. The idea is to prolong whenever possible the already reached sequences of concrete transitions, and to parameterize the order in which the states and actions occur. This concrete under-approximation ends up covering partially (at best totally) the reachable abstract transitions. The computed tests are paths of the under-approximation. The paper also reports on an implementation, which permits to provide experimental results confirming the interest of the approach with related heuristics.

In the actual business world, companies rely more and more on workflows to model the core of their business processes. In this context, the focus of workflow analysts is made on the verification of workflows specifications, in particular of modal specifications that allow the description of necessary or admissible behaviors. The design and the analysis of business processes commonly relies on workflow nets, a suited class of Petri nets. The goal of this paper is to evaluate and compare in a deep way two resolution methods—satisfiability modulo theory and constraint logic programming—applied to the verification of modal specifications over workflow nets. Firstly, it provides a concise description of the verification methods based on constraint solving. Secondly, it introduces the toolchain developed to automate the full verification process. Thirdly, it describes the experimental protocol designed to evaluate and compare the scalability and efficiency of both resolution approaches and reports on the obtained results. Finally, these obtained results are discussed in detail, lessons learned from these experiments are given, and, on the basis of experiments feedback, directions for improvement and future work are suggested.

On a partially observed system, a secret φ is opaque if an observer cannot ascertain that its trace belongs to φ. We consider specifications given as Constraint Markov Chains (CMC), which are underspecified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest scheduler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.

In test generation, when computing a reachable concrete under-approximation of an event system's predicate abstraction, we aim at covering each reachable abstract transition with at least one reachable concrete instance. As this is in general undecidable, an algorithm must finitely instantiate the abstract transitions for it to terminate. The approach defended in this paper is to first concretely explore the abstract graph, while concretizing the abstract transitions met at most once. However, some abstract transitions would require that loops were taken previously for them to become reached. To this end, in a second phase, a test engineer guides the exploration by describing a relevance predicate able to travel such loops. We give hints on how to design and express a relevance predicate, and provide a method for automatically extracting a variant out of it. A relevance guided concretization algorithm is given, whose termination is ensured by using this variant. Experimental results are provided that show the interest of the approach.

Model-based testing of event systems can take advantage of considering abstractions rather than explicit models, for controlling their size. A test is then a connected and reachable event sequence. This paper reports on experiments made when adapting for event systems two known under-approximation techniques of predicate tri-modal (may, must+, must-) abstractions. We first instantiate all the abstract may transitions, preferably as reachable instances. Second, we complete this underapproximation with instantiations of Ball chains, i.e. sequences in the shape of must-*. may. must+* transitions, as such sequences are guaranteed to have connected instantiations. We present a backward symbolic instantiation algorithm for connecting these two under-approximations. We experimentally address the question of their complementarity. Surprisingly, our results show that Ball chains have not enhanced the coverage already achieved by the first step of may-transitions instantiation. However, it has enhanced the number of test steps by prolonging the already existing tests.

Component-based systems permit standardisation and re-usability of code through the use of components. The architecture of component-based systems can be modified thanks to dynamic reconfigurations, which contribute to systems’ (self-)adaptation by adding or removing components without incurring any system downtime. In this context, the present article describes a formal model for dynamic reconfigurations of component-based systems. It provides a way of expressing runtime reconfigurations of a system and proving their correctness according to a static invariant for consistency constraints and/or a user-provided post-condition. Guarded reconfigurations allow us to build reconfigurations based on primitive reconfiguration operations using sequences of reconfigurations and the alternative and the repetitive constructs, while preserving configuration consistency. A practical contribution consists of the implementation of a component-based model using the GROOVE graph transformation tool. This implementation is illustrated on a cloud-based multi-tier application hosting environment managed as a component-based system. In addition, after enriching the model with interpreted configurations and reconfigurations in a consistency compatible manner, component systems’ implementations are related to their specifications by a simulation relation.

Dans les systemes evenementiels le flot de controle est implicite. Par consequent leur abstraction peut engendrer des traces deconnectees et inatteignables depuis l'etat initial. Cet article presente une methode algorithmique permettant le calcul d'une sous-approximation connectee et atteignable de l'abstraction d'un systeme evenementiel. La sous-approximation est calculee avec des instances concretes des transitions abstraites d'une abstraction par predicats, dans l'objectif d'en couvrir tous les etats et toutes les transitions. Pour etre utilisables, ces transitions concretes doivent etre atteignables et connectees les unes aux autres. Cet article propose une methode permettant d'instancier chaque transition abstraite a l'aide d'heuristiques favorisant leur connectivite. Cet article confirme l'interet de l'approche par des resultats experimentaux comparant la methode sans heuristique et avec.

This paper proposes a reduction method to verify the generalised soundness of large workflows described as workflow nets–a suited class of Petri nets. The proposed static analysis method is based on the application of six novel reduction transformations that transform a workflow net into a smaller one while preserving generalised soundness. The soundness of the method is proved. As practical contributions, this paper presents convincing experimental results obtained using a dedicated tool, developed to validate and demonstrate the effectiveness, efficiency and scalability of this method over a large set of industrial workflow nets.

The model of tree automata with equality and disequality constraints was introduced in 2007 by Filiot, Talbot and Tison. In this paper we show that if there is at least one disequality constraint, the emptiness problem is NP-hard.