MTV2 – 7 décembre 2018

 Pascale Le Gall 

 

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

La prochaine réunion du groupe MTV2 du GDR GPL aura lieu le 7 décembre 2018 à l’ENSIIE à Evry, et sera associée à la réunion du groupe LTP (Langages, Types, Preuves) qui aura lieu la veille (6 décembre) au même endroit.

Pour se rendre à l’ENSIIE, consultez la page.

Inscriptions

Les inscriptions sont toujours en cours  directement sur la page  : https://doodle.com/poll/ndqgg3bcc939q786

Programme préliminaire

(les titres et résumés des exposés sont fournis en bas de la page)

9h00-9h30 Welcome Coffee / Accueil – café

9h30-10h50 Session 1 (3x25min, 20 min exposé + 5 min questions)

  • Nikolai Kosmatov, Pascale Le Gall, Opening/Ouverture de la journée (5min.)
  • Antoine Rollet (Université de Bordeaux)
  • Mathieu Collet (Simula)
  • Zitoun Heytem (Université de Nice)

10h50-11h15 Coffee Break / Pause café

11h15-12h30 Session 2 (25min+50min, 20 min ou 45 min exposé + 5 min questions)

  • Léo Henry (IRISA)
  • Invited talk. Bernhard Aichernig (Graz University of Technology, Austria)  “Smart Black-box Testing – Combining Model Learning and Model-based Testing”

12h30-14h00 Lunch / Déjeuner

14h00-15h15 Session 3 (conférencier invité)  (50min+25min, 45 min ou 20 min exposé + 5 min questions

  • Invited talk. Mike Papadakis (Univ. Luxembourg) “Mutation Testing Advances”
  • Fonenantsoa Maurica (CEA List)

15h15-15h40 Coffee Break / Pause café

15h40-16h55 Session 4 (3x25min, 20 min exposé + 5 min questions)

  • Gabriel Radanne (Université de Freiburg)
  • Asma Berriri (TSP)
  • Sylvain Hallé (Université du Québec à Chicoutimi)

16h55-17h00 Announcements / Annonces, fin de journée

Conférenciers invités

Michail Papadakis (SnT, University of Luxembourg https://sites.google.com/site/mikepapadakis)

Mutation Testing Advances

Résumé : Mutation testing realises the idea of using artificial defects to support testing activities. Mutation is typically used as a way to evaluate the adequacy of test suites, to guide the generation of test cases and to support experimentation. Mutation has reached a maturity phase and gradually gains popularity both in academia and in industry. This talk will survey the advances related to the fundamental problems of mutation testing, will set out the challenges and open problems for the future development of the method and will present ongoing industrial projects using mutation testing.

Bio : Dr. Papadakis is a research scientist at the Interdisciplinary Center for Security, Reliability and Trust (SnT) at the University of Luxembourg. He received a Ph.D. diploma in Computer Science from the Athens University of Economics and Business. He is recognised for his work on mutation testing. He recently published a survey on mutation testing advances and maintains a related repository with more than 800 publications (related to mutation testing). He has been on the program and organization committees of many international software engineering conferences (e.g., ICSE, ICST, SSBSE and QRS) and serves at the Editorial Board of the STVR journal. His research interests include software testing, static analysis, prediction modelling, mutation analysis and search-based software engineering.

Bernhard Aichernig  (IST, TU Graz, Autriche  http://aichernig.blogspot.com)

Smart Black-box Testing – Combining Model Learning and Model-based Testing

Résumé :Testing has always been a challenge due to (1) its incompleteness by nature, (2) the lack of good specifications and (3) by its high demand for resources. With the growing complexity of the systems-under-test the situation is not likely to improve. The combination of model-learning with model-based testing offers an opportunity to master this complexity. In my talk I will introduce this line of research and report about our recent results including applications in the Internet of Things. We will discuss the learning and testing of several classes of models/systems including Mealy machines, Markov decision processes and timed automata. Our goal is a natural evolution of testing: with the trend of our environment becoming « smarter », e.g. smart homes, smart cars, smart production, smart energy, our testing process should become smart as well. We are seeing the advent of smart testing.

Bio : Bernhard K. Aichernig is a tenured associate professor at Graz University of Technology, Austria. He investigates the foundations of software engineering for realising dependable computer-based systems. Bernhard is an expert in formal methods and testing. His research covers a variety of areas combining falsification, verification and abstraction techniques. Current topics include the Internet of Things, model learning, and statistical model checking. Since 2006, he participated in four European projects. From 2004-2016 Bernhard served as a board member of Formal Methods Europe, the association that organises the Formal Methods symposia. From 2002 to 2006 he had a faculty position at the United Nations University in Macao S.A.R., China. Bernhard holds a habilitation in Practical Computer Science and Formal Methods, a doctorate, and a diploma engineer degree from Graz University of Technology.

Titres et résumés

Asma Berriri — Formal approaches for verification and testing in virtual networks

This work is focused on the use of formal models for the effective testing and verification of virtual (programmable) networks, and in particular Software Defined Networking (SDN) frameworks as a whole as well as their particular OpenFlow (OF) components. Firstly, we propose novel techniques for testing the entire SDN architectures taking into account potential interoperability issues in the controller-to-switch communication. The proposed model based testing technique relies on appropriate graph enumeration. Secondly, we propose model based techniques for testing critical SDN components, in particular, SDN-enabled switches. On one hand, we are interested in testing the forwarding functionality of the switch modelled and analyzed as a ‘stateless’ system. Appropriate logic circuits are proposed to model the switch behavior then both active and passive testing modes can be considered. On the other hand, we focus on testing the switch modelled as a ‘stateful’ system and taking into account its communication with the controller. An Extended Finite State Machine (EFSM) model is generated from the OF specification and mutation testing is applied. Appropriate fault models are introduced and test suites with guaranteed fault coverage are derived. Furthermore, a testing environment is developed. The performed experimental study shows the efficiency of the proposed test generation and verification techniques in testing the whole SDN architecture and the derived test suites are able to detect a number of functional inconsistencies in available OF switch implementations.

Sylvain Hallé — BeepBeep, ou le traitement de flux d’événements facile et flexible

Beaucoup de problèmes courants en informatique peuvent être vus comme une forme de traitement appliqué à une séquence d’objets –un flux d’événements. Par exemple, on peut instrumenter un programme et analyser en temps réel si son exécution est conforme à une spécification, ce que l’on appelle runtime verification. Dans cette courte présentation, on verra le fonctionnement de base et les applications possibles de BeepBeep, une librairie open source spécialisée dans l’expression de chaînes de traitement variées sur des flux d’événements d’origines diverses. Si le temps le permet, on verra comment BeepBeep a été utilisé pour monitorer des jeux vidéo, analyser des flux réseau, et imposer des contraintes de sécurité à des programmes Java

Leo Henry — Control strategies for off-line testing of timed systems

Partial observability and controllability are two well-known issues in test-case synthesis for interactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. Building on the tioco tuimed testing framework, we extend a previous game interpretation of the test-synthesis problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that tries to minimize both control losses and distance to the satisfaction of a test purpose, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method.

Zitoun Heytem — Stratégies de recherche pour les systèmes de contraintes sur les flottants

La vérification des programmes est un enjeu majeur pour les applications critiques comme l’aviation, l’aérospatiale ou les systèmes embarqués. Les approches Bounded model checking (e.g., CBMC) et de programmation par contraintes (e.g., CPBPV, ….) reposent sur la recherche de contre-exemples qui violent une propriété du programme à vérifier. La recherche de tels contre-exemples peut être très longue et coûteuse lorsque les programmes à vérifier contiennent des calculs en virgule flottante. Ceci est dû en grande partie au fait que les stratégies de recherche existantes ont été conçues pour des domaines finis et, dans une moindre mesure, pour des domaines continus. Nous avons proposé un ensemble de stratégies de recherche dédiées à la vérification de programme avec du calcul sur les flottants.  Les stratégies proposées pour les choix de variables se basent sur des propriétés propres aux domaines des variables (e.g., densité des domaines ) et aux contraintes sur les flottants (e.g., arithmétique propre aux flottants et structure même des problèmes). Les stratégies de choix de valeurs ciblent quant à elle les sous-domaines impliqués dans une absorption. L’évaluation de ces stratégies sur un ensemble de programmes réalistes est très encourageante : ces stratégies sont plus efficaces que les stratégies standards.

Fonenantsoa Maurica — Runtime Assertion Checking with Frama-C/E-ACSL: the \at Construct

Runtime Assertion Checking (RAC) consists in launching a program then determining during its execution whether it meets its requirements. These requirements are often expressed in a dedicated formal specification language. RAC complements static analysis techniques which offer stronger guarantees but at the cost of greater verification efforts. RAC also complements testing techniques by checking finer properties than the latter. In this talk, we present the Frama-C/E-ACSL tool for performing RAC on C programs. In particular, we focus on the challenges raised by the \at(x,L) construct of its specification language. It refers to the value of x at program point L. This construct is central, at least, to function contracts where the result (at the end) of a function is to be expressed in terms of the values of its arguments (at its beginning).

Gabriel Radanne — Regenerate: A Language Generator for Extended Regular Expressions, with an application to test case generation

Regular expressions are part of every programmer’s toolbox. They are used for a wide variety of language-related tasks and there are many algorithms for manipulating them. In particular, matching algorithms that detect whether a word belongs to the language described by a regular expression are well explored, yet new algorithms appear frequently. However, there is no satisfactory methodology for testing such matchers. We propose a testing methodology which is based on generating positive as well as negative examples of words in the language. To this end, we present a new algorithm to generate the language described by a generalized regular expression with intersection and complement operators. The complement operator allows us to generate both positive and negative example words from a given regular expression. We implement our generator in Haskell and OCaml and show that its performance is more than adequate for testing. Site Web: https://regex-generate.github.io/regenerate/

Antoine Rollet — Enforcement à l’exécution de propriétés (temporisées) avec événements incontrôlables

L’enforcement à l’exécution regroupe les techniques mises en œuvre pour garantir que l’exécution d’un système est conforme à une spécification donnée. Dans cet exposé, nous présenterons quelques résultats concernant l’enforcement à l’exécution de propriétés régulières en présence d’événements incontrôlables, i.e. des événements qui ne peuvent être modifiés par le mécanisme d’enforcement. Nous présenterons notre approche dans un cadre non temporisé, et nous verrons comment étendre ces résultats dans un cadre temporisé.

Organisateurs

Nikolai Kosmatov (CEA LIST)

Pascale Le Gall (MICS, CentraleSupélec)