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.

Our objective is to define a regression testing approach that relies on usage traces that capture the behaviours of the system when exploited by the users. We achieve that by studying and evaluating clustering techniques applied to usage traces for regression tests selection. We first evaluate the existing vectorization methods and the clusters computed by the classical algorithms, and then, evaluate the clusters using existing state-of-the-art validation methods. We conclude that neither the existing clustering algorithms, nor the seminal clustering evaluation techniques are well-suited for identifying representative behaviours of the system when applied to usage traces. Thus, we propose a custom clustering algorithm and a dedicated cluster evaluation index for selecting usage trace to be used as regression tests.

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.

We present, in this paper, teaching material and experience report on teaching software testing to 3rd year bachelor's degree students. Our approach covers a wide range of techniques from unit testing, to functional testing, through test-first design and black-box testing. To motivate students, we rely on the use of a running case study, that is developed and tested all the way through. This paper presents both teaching material and experience report based on the feedback that we get from the students, and the observations we made regarding the discovery of the software testing aspects.

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.

Testing IT systems has become a major bottleneck for many companies. Besides the growing complexity of such systems, shorter release cycles and increasing quality requirements have led to increased verification and validation costs. However, analysis of existing testing procedures reveals that not all artifacts are exploited to tame this cost increase. In particular, customer traces are usually ignored by validation engineers. In this paper, we use machine learning from execution traces (both customer traces and test execution traces) to identify test needs and to generate new tests in the context of web services and API testing. Log files of customer traces are split into smaller traces (user sessions) then encoded into Pandas DataFrames for data analysis and machine learning. Clustering algorithms are used to analyse the customer traces and compare them with existing system tests, and machine learning models are used to generate missing tests in the desired clusters. The tool-set is implemented in an open-source library called Agilkia.

This article presents a successful industrial application of a model-based testing approach to the validation of security components. We present a smart combination of three test selection criteria applied to testing security requirements of components such as Hardware Security Modules. This combination relies on the use of static test selection criteria, namely structural model coverage, complemented by dynamic test selection criteria, based on abstract test scenarios or temporal properties, designed to target corner cases of security functional requirements. Our approach is implemented in an industrial and scalable MBT tool. We evaluated and successfully applied it on three real-world security components. The outcome of these experiences showed that the three test selection criteria target distinct kinds of errors in the software and are able to reveal inconsistencies in the specification. Moreover, a 5-year experience of working with both manufacturers and evaluators of security components, along with other industrial collaborations, showed that the approach is easy to adopt in the industry and the time spent to learn the methodology is negligible with respect to its benefits. Finally, the approach can be completely applied in a more general context on systems that underlay thorough validation of compliance to specifications or audits.

This article describes a new property- and model-based testing approach using UML/OCL models, driven by temporal property patterns and a tool for assisting the temporal properties formalization. The patterns are expressed in the TOCL language, an adaptation of Dwyer's property patterns to OCL. The patterns are used to formalize temporal requirements without having to learn a complex temporal logics such as LTL or CTL. From these properties, automata are automatically computed. These can be used for two purposes. First, it is possible to evaluate the quality of a test suite by measuring the coverage of a property using its associated automaton. Second, the automaton can be used to drive the test generation in order to produce complementary test cases. To this end, we defined dedicated coverage criteria, targeting specific events of the property, and aiming either at illustrating the expected behaviour of the system, or checking its robustness w.r.t. the property. However, it was observed that the semantics of the property language may be more subtle that it seems. To facilitate the adoption of the language by industrials, we have proposed a tool-supported assistant for property design, aiming to help the validation engineer choosing which constructs faithfully correspond to his intention. This approach has been experimented on several case studies with industrial partners. It has shown its interest for software validation, providing useful information thanks to adequate traceability features.

We summarize several contributions related to the PHP Realistic Annotation and SPEcification Language (Praspel). This language extends PHP programs with annotations for the formal specification of the behavior of their functions and for the declaration of types for their data. These contracts are used to automate test generation, by deriving test cases and test data, and test execution, by checking assertions at run-time in order to establish the test verdict. Our approach to contract-based testing for PHP is fully implemented into a PHP framework currently in use by several web companies. (C) 2017 Elsevier Inc. All rights reserved.

Evolution and dispersion history on Earth of organisms can best be studied through biological markers in molecular epidemiological studies. The biological diversity of the cestode Echinococcus multilocularis was investigated in different cladistic approaches. First the morphological aspects were explored in connection with its ecology. More recently, molecular aspects were investigated to better understand the nature of the variations observed among isolates. The study of the tandemly repeated multilocus microsatellite EmsB allowed us to attain a high genetic diversity level where other classic markers have failed. Since 2006, EmsB data have been collected on specimens from various endemic foci of the parasite in Europe (in historic and newly endemic areas), Asia (China, Japan and Kyrgyzstan), and North America (Canada and Alaska). Biological data on the isolates and metadata were also recorded (e.g. host, geographical location, EmsB analysis, citation in the literature). In order to make available the data set of 1,166 isolates from classic and aberrant domestic and wild animal hosts (larval lesions and adult worms) and from human origin, an open web access interface, developed in PHP, and connected to a PostgreSQL database, was developed in the EmsB Website for the Echinococcus Typing (EWET) project. It allows researchers to access data collection, perform genetic analyses online (e.g. defining the genetic distance between their own samples and the samples in the database), consult distribution maps of EmsB profiles, and record and share their new EmsB genotyping data. In order to standardize the EmsB analyses performed in the different laboratories throughout the world, a calibrator was developed. The final aim of this project was to gather and arrange available data to permit to better understand the dispersion and transmission patterns of the parasite among definitive and intermediate hosts, in order to organize control strategies on the ground.

This talk presents results recently published in Software Testing, Verification and Reliability. In recent years, important efforts have been made for offering a dedicated language for modelling and verifying/proving security protocols. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. In this talk we present a model-based testing approach, relying on the mutation of HLPSL - the specification language of the AVISPA tool - models to generate abstract test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real-world implementation errors.

In the recent years, important efforts have been made for offering a dedicated language for modelling and verifying security protocols. Outcome of the European project AVISPA, the High-Level Security Protocol Language (HLPSL) aims at providing a means for verifying usual security properties (such as data secrecy) in message exchanges between agents. Nevertheless, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. We propose in this paper a testing technique that makes it possible to validate an implementation of a security protocol, based on a HLPSL model. We introduce a set of mutation operators for HLPSL models that aim at introducing leaks in the security protocols. The mutated models are then analysed by the AVISPA tool set that will produce counter-example traces leading to the leaks, thus providing the test cases. We report an experiment of our mutation technique on a wide range of security protocols and discuss the relevance of the proposed mutation operators.

Dwyer et al. provide a language to specify dynamic properties based on a limited number of predefined patterns and scopes. The semantics of these properties is defined by translating each combination of a pattern and a scope into usual temporal logics (linear temporal logic, CTL, etc.). This translational semantics suffers from two main issues. It is not easily extensible to other patterns or scopes, and it is not always faithful to the natural semantics. In this article, we propose a compositional automata-based approach defining the semantics of each pattern and each scope by an automaton, after which the semantics is composed. Hence, the semantics is compositional and the language is easily extensible. We compare the two semantics by model checking. In some cases, our semantics reveals a lack of homogeneity within Dwyer et al.’s semantics. Finally, we apply this approach in the context of property-based testing, in order to evaluate the quality of a test suite, by measuring the coverage of the property automaton. To allow the tester to adapt the coverage criteria to its goals, we propose transformation rules over the patterns automata that implement relevant unfolding strategies for loops, or predicates labeling the automata transitions. We illustrate these principles by means of an industrial case study.

We investigate an approach to automate model-based vulnerability testing of payment protocols used by e-commerce applications. We aim to improve the efficiency and performance of logical vulnerability testing. The proposed approach is based on a formal specification of the protocol implementation (SUT) and vulnerability attack scenario exploitation for driving the test execution. This approach is illustrated with a use case example bookshop application and one of the most used payment protocols: PayPal Express.

Ce document dresse un bilan des defis identifies par le groupe de travail Methodes de Test pour la Verification et la Validation (MTV2) lors de l'appel lance par le GDR GPL en 2010. Pour chaque defi initialement identifie, nous evaluons si des reponses ont ete apportees durant ces 4 dernieres annees, nous presentons les eventuelles avancees realisees, et proposons le cas echeant de nouveaux defis lies aux technologies emergentes.

Cross-Site Scripting (XSS) vulnerability is one of the most critical breaches that may compromise the security of Web applications. Reflected XSS is usually easy to detect as the attack vector is immediately executed, and classical Web application scanners are commonly efficient to detect it. However, they are less efficient to discover multi-step XSS, which requires behavioral knowledge to be detected. In this paper, we propose a Pattern-driven and Model-based Vulnerability Testing approach (PMVT) to improve the capability of multi-step XSS detection. This approach relies on generic vulnerability test patterns, which are applied on a behavioral model of the application under test, in order to generate vulnerability test cases. A toolchain, adapted from an existing Model-Based Testing tool, has been developed to implement this approach. This prototype has been experimented and validated on real-life Web applications, showing a strong improvement of detection ability w.r.t. Web application scanners for this kind of vulnerabilities.

We present an integrated contract-based testing framework for PHP. It relies on a behavioral interface specification language called Praspel, for Realistic Annotation and Specification Language. Using Praspel developers can easily annotate their PHP scripts with formal contracts, namely class invariants, and method pre- and postconditions. These contracts describe assertions either by predicates or by assigning realistic domains to data. Realistic domains introduce types in PHP and describe complex structures frequently encountered in applications, such as email addresses or SQL queries. Realistic domains display two properties: predicability, which allows to check if a data belongs to a given realistic domain, and samplability, which allows to generate valid data. This paper introduces coverage criteria dedicated to contracts, designed to exhibit relevant behaviors of the annotated methods. Test data are then computed to satisfy these coverage criteria, by using dedicated data generators for complex realistic domains, such as arrays or strings. This framework has been implemented and disseminated within the PHP community, which gave us feedback on their usage of the tool and the relevance of this integrated process with respect to their practice of manual testing.

We present in this paper a model-based testing approach aiming at generating test cases from a UML/OCL model and a given test property. The property is expressed using a dedicated formalism based on patterns, and automatically translated into an automaton. We propose new automata coverage criteria that are tailored to the property automata we consider. These criteria are based on the coverage of a relevant subset of the transitions related to the original property, aiming at producing test cases that illustrate the dynamics of the system described in the property. In addition, we propose to produce test cases that can ensure the robustness of the system w.r.t. the property, by mutating the property automaton, in order to try to provoke events that would be forbidden by the property. This approach has been implemented into a large tool set and it has been experimented on realistic case studies, in the context of industrial research projects.