Groupe de travail

Méthodes de Test pour la Vérification et la Validation
MTV2

Réunion MTV2 du 3 décembre 2014 à Supélec - Saclay/Gif-sur-Yvette

La prochaine réunion du groupe aura lieu le mercredi 3 décembre 2014 dans les locaux de Supélec à Gif-sur-Yvette.

Cette réunion est soutenue par le GDR GPL.

Pour vous inscrire, envoyez un mail à l'organisateur local : Safouan Taha, en précisant les nom, prénom, institution, adresse complète, téléphone et email des participants.

Venir à Supélec

La réunion aura lieu sur le site de Supélec à Gif-sur-Yvette, 3 rue Joliot-Curie.

Le plan et les moyens d'accès au site sont donnés à l'adresse : http://www.supelec.fr/388_p_12022/plan-d-acces.html

Programme

Session 1 - 10h30-12h

  • Nikolai Kosmatov, Matthieu Lemerre, Céline Alec
    A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing.
    Complete formal verification of software remains extremely expensive and often reserved in practice for the most critical products. Test generation techniques are much less costly and can be used in combination with theorem proving tools to provide high confidence in the software correctness at an acceptable cost when an automatic prover does not succeed alone. This work presents a case study on verification of a cloud hypervisor with the Frama-C toolset, in which deductive verification has been advantageously combined with structural all-path testing. We describe our combined verification approach, present the adopted methodology and emphasize its benefits and limitations.

  • Mickaël Delahaye
    An All-in-One Toolkit for Automated White-Box Testing
    Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations.
    Joint work with Sébastien Bardin, Nikolai Kosmatov and Omar Chebaro.

  • Diego Rivera
    Integrating Business Parameters for QoE Evaluation of OTT Services Based on TEFSMs
    Most of the work related to QoE maps objective variables (QoS-related) into a single one that predicts the quality the users perceives. In this presentation we present a new approach to model multimedia OTT services, integrating not only the functional aspects of the service but also non-functional variables, which are classified into objective, subjective and business-related. Non-functional metrics might affect the Quality of Service (QoS), Quality of Experience (QoE) and Quality of Business (QoBiz) correspondingly. We also discuss how all these variables can be taken into account to predict the QoE of the service being studied. The functional requirements are modeled into a Time Extended Finite States Machine (TEFSM), which is augmented with context variables (and their updating functions) representing non-functional requirements related to QoS, QoE and QoBiz. We use these parameters to evaluate the QoE using a trace model derived from the TEFSM previously built.

Session 2 - 14h-15h30

  • Steven De Oliveira
    Vérification de propriétés temporelles sur des programmes C.
    Le (bon) séquencement des événements au fil du temps est un sujet important pour l'analyse de programmes, par exemple dans le cadre de protocoles d'échange d'information ou de systèmes embarqués. De nombreux travaux s'appuient sur la logique temporelle linéaire (LTL) pour décrire formellement le comportement attendu d'un programme, sous la forme d'une succession d’actions distinctes. Cet article présente CaFE, un outil vérifiant automatiquement de manière approchée (mais correcte) qu'un programme C vérifie une formule logique CaRet donnée, où CaRet est une extension de LTL permettant en particulier de raisonner explicitement sur la pile d'appel du programme.

  • Jorge Lopez
    Behavior Evaluation for Trust Management based on Formal Distributed Network Monitoring.
    Collaborative systems are growing in use and popularity. The need to boost the methods concerning the interoperability is growing as well; therefore, trustworthy interactions of the different systems are a priority. The decision regarding with whom and how to interact with other users or applications depends on each system. We focus on providing trust verdicts by evaluating the behaviors of different agents, using distributed network monitoring. This will provide trust management systems information regarding a trustee experience, for those trust management systems based on "soft trust". We propose a formal distributed network monitoring approach to analyze the packets exchanged by the entities, to prove a system is acting in a trustworthy manner. Based on formal "trust properties", we analyze the systems' behaviors, then, we provide trust verdicts. Aautomatized testing is performed using a suite of tools we developed and we have proved our methodology in an industrial, real-case scenario.

  • Alexandre Vernotte
    Génération de test de vulnérabilité Web à partir de modèles et dirigée par des patterns de test
    Les Scanners de vulnérabilité Web permettent de détecter une majorité de vulnérabilités, apportant ainsi un premier niveau de confiance. Cependant, ces outils automatiques souffrent de faux positifs et faux négatifs lorsqu'il s'agit de détecter des vulnérabilités complexes comme le multi-step XSS, ou des vulnérabilités logiques comme des références directes non sécurisées à un objet. Nous proposons ainsi une approche de test de vulnérabilité à partir de modèles et pilotée par des patterns de test, pour améliorer la capacité de détection du test de vulnérabilité. Cette approche s'appuie sur des patterns de test génériques appliqués à un modèle comportemental de l'application sous test pour générer des cas de test de vulnérabilité. Une chaîne outillée, basée sur un outil MBT existant, a été développée et expérimentée sur plusieurs applications réelles. Ce prototype montre une amélioration de la capacité de détection des vulnérabilités complexes et logiques lorsque comparé aux scanners du marché.

Session 3 - 16h-17h

  • Nassim Benharrat
    Communication checking for Model-based testing of distributed systems
    Many systems interact with their environment at physically distributed interfaces and the distributed nature of any observation is known to complicate testing. A classical testing architecture consists in considering a separate tester at each localized interface that can only observe what happens at this interface. Each localized system is modelled using a timed input output transition system (TIOTS). Different events (observations or stimulations) occurring at different interfaces cannot be ordered anymore since it is not possible to compare their respective moments at which they occurred. Indeed, we assume that there is no global clock for the whole system but only local clocks for each localized subsystem. Furthermore, we assume that local testers cannot communicate with each other. Semantics of such systems can be seen as tuples of traces (one component per localized system representing a local vision of the subsystem in question) and a conformance relation called input-output conformance relation (ioco) is defined with respect to tuples of localized traces. The conformance relation ioco expresses that a System Under Test (SUT) conforms to its specification if the SUT never produces an output that cannot be produced by the specification. Timed input-output conformance relation (tioco) is an extension of ioco that includes time delays in the set of the outputs. A distributed system conforms to a model if each local subsystem conforms to the corresponding TIOSTS model and if communications between local subsystems are consistent with respect to the passage of time and with the coupling of emission and reception of internal message. Communication consistency is defined through some rules leading to an algorithm for checking communication consistency.

  • Annonces : journées du GDR 2015, conférence AFADL, suite du groupe de travail.