Search

[EN] Context: Over the last 30 years, GUIs have changed considerably, becoming everyday part of our lives through smart phones and other devices. More complex GUIs and multitude of platforms have increased the challenges when testing software through the GUI. Objective: To visualise how the field of automated GUI testing has evolved by studying the growth of the field; types of publications; influential events, papers and authors; collaboration among authors; and trends on GUI testing. Method: To conduct a bibliometric analysis of automated GUI testing by performing a systematic search of primary studies in Scopus from 1990 to 2020. Results: 744 publications were selected as primary studies. The majority of them were conference papers, the most cited paper was published on 2013, and the most published author has 53 papers. Conclusions: Automated GUI testing has continuously grown. Keywords show that testing applied to mobile interfaces will be the trend in next years, along with the integration of Artificial Intelligence and automated exploration techniques., We thank Fernando Pastor for his valuable contribution. This research has been funded by DECODER (decoder-project.eu), iv4XR (iv4xrproject.eu), and IVVES (ivves.weebly.com) projects.

International audience; Our objective is to increase the individual throughput of each node in the network by exploiting neighbors with more favorable channel conditions in terms of bit rate and packet loss ratio. We propose a per-neighbor message queue in order to reduce the effect of the Head Of Line (HOL) blocking problem of IEEE 802.11. A weighted queuing scheduler grants each neighbor a service proportional to its channel conditions. The sender maintains a separate backoff counter for each neighbor and adopts a dynamic binding strategy to avoid multiple transmissions to a neighbor with bad channel conditions. We use a continuous time Markov chain model to study the proposed mechanism and to derive the correspondent parameters optimizing the channel utilization. The Matlab simulations show good expected performance gain compared to the standard implementation of IEEE 802.11

National audience; L'utilisation de modélisations formelles est devenue une partie intégrante du processus de développement de logiciels sûrs. En effet, une bonne modélisation du système à développer permet d'améliorer la qualité des logiciels en détectant, par exemple, certaines vulnérabilités avant même leurs déploiements. Dans cette optique, ce papier propose une nouvelle méthode de modélisation de vulnérabilités ainsi qu'un langage formel pour l'expression précise sans ambiguïté des causes et événements pouvant les produire. La définition d'un tel langage formel permet également la détection automatique des vulnérabilités par des outils de test. Plus précisément, nous illustrons l'utilisation de l'outil de test passif TestInv, développé au sein de notre équipe, pour la détection automatique de vulnérabilités exprimées dans le langage formel ainsi défini. Notre approche a l'avantage de produire un nombre beaucoup plus réduit de faux positifs tout en maintenant à jour la base de connaissances de l'outil TestInv. L'approche proposée est illustrée à travers l'exemple de vulnérabilité CVE-2005-3192 représentant un ``buffer overflow" dans un programme C

International audience; The C language is widely used for developing tools in various application areas, and a number of C software tools are used for critical systems, such as medicine, transport, etc. Correspondingly, the security of such programs should be thoroughly tested, i.e., it is important to develop techniques for detecting vulnerabilities in C programs. In this paper we present an approach for dynamic detection of software vulnerabilities using the SPIN model checker. We discuss how this approach can be implemented in order to detect automatically C code vulnerabilities and illustrate a proposed technique for a number of C programs which are widely used in a number of applications

Software-intensive safety critical systems are becoming more and more widespread and are involved in many aspects of our daily lives. Since a failure of these systems could lead to unacceptable consequences, it is imperative to guarantee high safety standards. In practice, as a way to handle their increasing complexity, these systems are often modelled as hierarchical systems. To date, a good deal of work has focused on the definition and analysis of hierarchical modelling languages and on their integration within model-driven development frameworks. Less work, however, has been directed towards formalisms to effectively express, in a precise and rigorous way, relevant behavioural properties of such systems (e.g.: safety requirements). In this work, we propose a novel extension of classic Linear Temporal Logic (LTL) called Hierarchical Linear Temporal Logic (HLTL), designed to express, in a natural yet rigorous way, behavioural properties of hierarhical systems. The formalism we propose does not commit to any specific modelling language, and can be used to predicate over a large variety of hierarchical systems.

The Multi-access Edge Computing (MEC) computing model provides on-demand cloud resources and services to the edge of the network, to offer storage and computing capacity, mobility, and context awareness support for emerging Internet of Things (IoT) applications. On the other hand, its complex hierarchical model introduces new vulnerabilities, which can influence the security of IoT applications. The use of different enabling technologies at the edge of the network, such as various wireless access and virtualization technologies, implies several threats and challenges that make the security analysis and the deployment of security mechanisms a technically challenging problem. This paper proposes a technique to model Edge-based systems and automatically extract security threats and plan possible security tests. The proposed approach is tested against a simple, but significant case study. The main contribution consists of a threat catalog that can be used to derive a threat model and perform a risk analysis process of specific MEC-based IoT scenarios.

Part 6: Short Contributions; International audience; Cyber-physical systems (CPS) are hybrid systems that commonly consist of a discrete control part that operates in a continuous environment. Hybrid automata are a convenient model for CPS suitable for formal verification. The latter is based on reachability analysis of the system to trace its hybrid evolution and consequently verify its properties. However, when computing reachable states, a challenging task especially for nonlinear noisy systems is to control automatically the numerical precision to obtain meaningful approximations of the reached set. This paper presents the ongoing work and open issues in the automated computation of system evolution when the dynamics is described by differential inclusions. Differential inclusions allow to model noise for hybrid systems and also to decouple the components in a complex system, in order to simplify model-based design and verification. The proposed work aims to extend the capabilities of Ariadne, a C++ library to perform formal verification of nonlinear hybrid systems.

Part 6: Short Contributions; International audience; In this paper, we investigate how a checking sequence can be generated from a Finite State Machine, with respect to a user-defined set of faults, modeled as a nondeterministic FSM, called Mutation Machine (MM). We propose an algorithm for generating a checking sequence in this scenario and demonstrate its correctness.

Part 4: Test Selection and Quality Estimation; International audience; Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in system testing and verification. Unlike prior methods based on explicit tree based search, in this work we formulate the derivation of a preset homing sequence in terms of a quantified Boolean formula (QBF). The formulation allows implicit NFSM representation and compact QBF encoding for effective computation. Different encoding schemes and QBF solvers are evaluated for their suitability to homing sequence derivation. Experimental results show the generality and feasibility of the proposed method.

Part 5: Testing Timed and Distributed Systems; International audience; We present GREP, a tool for the runtime enforcement of (timed) properties. GREP takes an execution sequence as input (stdin), and modifies it (stdout) as necessary to enforce the desired property, when possible. GREP can enforce any regular timed property described by a deterministic and complete Timed Automaton. The main novelties of GREP are twofold: it uses game theory to improve the synthesis of enforcement mechanisms, and it accounts for uncontrollable events, i.e. events that cannot be controlled by the enforcement mechanisms and thus have to be released immediately. We present an overview of GREP and validate its usability with a performance evaluation.

Part 2: Test Derivation Methods; International audience; The paper focuses on the problems of passive and active FSM inference as well as checking sequence generation. We consider the setting where an FSM cannot be reset so that its inference is constrained to a single trace either given a priori in passive inference scenario or to be constructed in active inference scenario or aiming at obtaining checking sequence for a given FSM. In each of the last two cases, the expected result is a trace representing a checking sequence for an inferred machine, if it was not given. We demonstrate that this can be achieved by a repetitive use of a procedure that infers an FSM from a given trace (identifying a minimal machine consistent with a trace) avoiding equivalent conjectures. We thus show that FSM inference and checking sequence construction can be seen as two sides of the same coin. Following an existing approach of constructing conjectures by SAT solving, we elaborate first such a procedure and then based on it the methods for obtaining checking sequence for a given FSM and inferring a machine from a black box. The novelty of our approach is that it does not use any state identification facilities. We only assume that we know initially the input set and a bound on the number of states of the machine. Experiments with a prototype implementation of the developed approach using as a backend an existing SAT solver indicate that it scales for FSMs with up to a dozen of states and requires relatively short sequences to identify the machine.

Part 3: Safety and Security Testing; International audience; The explosion of digitisation makes a plethora of security data publicly available for developers. These numerous (often complex) documents expose them to the difficulty of choosing the most appropriate solution for securing their applications. We propose in this paper a method based upon data acquisition and integration, which assists developers in the Threat modelling stage and in the security test case execution. The method firstly helps devise Attack Defense Trees by means of a data-store. These trees show attacks, steps and defenses given under the form of security patterns, which are re-usable solutions to design more secure applications. These trees are then used for the test case generation. The data-store integrates test case stubs, which make this generation easier and developers more efficient. We evaluate our approach on 24 participants and show encouraging results on the use of data integration in software engineering.

Part 6: Short Contributions; International audience; When testing a black box system that cannot be reset, it may be useful to use a localizer procedure that will ensure that the test sequence goes at some point through a state that can be identified with a characterizing set of input sequences. In this paper, we propose a procedure that will localize when the separating sequences are organized in a splitting tree. Compared to previous localizing sequences based on characterization sets, using the tree structure one can define an adaptive localizer, and the complexity of localizing depends on the height of the tree instead of the number of states.

Part 4: Test Selection and Quality Estimation; International audience; A virtual machine (VM) placement module is a component/part of a cloud (computing) infrastructure, which chooses the best host(s) to allocate the requested VMs. In the literature, skewed or biased criteria are often used to determine the correctness of a placement module. Therefore, the quality of existing placement solutions is not always assessed adequately. In this paper, we propose a distance function that estimates the quality of the placement by comparing it with an optimal solution. We show how this distance function is utilized for testing and monitoring the behavior of VM placement implementations. To validate our approach a simulator has been developed and used for estimating the quality of different placement modules running under various scenarios. Preliminary experimental results on VM placement algorithms implemented in widely used platforms, such as OpenStack show that very often VMs are placed very far from the optimal solutions.