!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 68nqrt Seminar - IRISA/Inria Rennes
Logo IRISA logo Inria

Prochain Exposé

June 30th, 3PM (Paris/France). Salle Markov

Helge Spieker (Simula Research Laboratory in Oslo, Norway)

The interplay of AI and software testing for resilient software systems.

AI-based software are of increasing relevance but also add additional challenges for the software testing process, such as the oracle problem of uncertainty in the precise expected outcome of the software or gigantic numbers of potential test scenarios. At the same time, AI techniques, both data-driven machine learning and logic-driven constraint solving, can aid testing techniques to be more cost-effective and focus on finding faults early. In this talk I will discuss a selection of applications at this intersection, involving metamorphic testing, reinforcement learning, and constraint optimization.

Exposés des semaines suivantes

July 19th, 10.30AM (Paris/France). Salle Markov. (in French)

Aurélie Hurault (INP Toulouse, IRIT)

Vérification de systèmes distribués asynchrone : exploration de la diversité des modèles asynchrones et du modèle Heard-Of

La présentation abordera deux séries de travaux autour de la vérification de systèmes distribués asynchrone.
Dans un premier temps, nous nous intéresserons à la formalisation des interactions asynchrones. Lors d’une preuve d’algorithme distribué, les propriétés sur la communication sont prouvées suffisantes pour la correction de l’algorithme. Cependant, il est souvent peu clair quelles sont ces propriétés de communication car elles sont généralement noyées au sein de l’algorithme. Il est notamment difficile de remplacer un modèle de communication par un autre sans avoir à refaire complètement la preuve ou le développement. Nous avons défini un cadre générique pour spécifier la diversité des modèles de communication asynchrone. Ce cadre permet de comprendre et comparer les différents modèles ainsi que de prouver la correction et la complétude de différentes définitions des modèles. Des modèles formels spécifiques de communications asynchrones ont été défini à l’aide d’Event-B et de TLA+ . Basé sur ces modèles, nous avons proposé un framework de vérification de compatibilité de systèmes distribués communiquant par messages asynchrones, en point à point ou en multicast. Il est mis à disposition en ligne : http://vacs.enseeiht.fr/
Dans un second temps, nous nous intéresserons aux défaillances. Plutôt que de formaliser chaque structure d’algorithme et chaque type de défaillance, nous nous restreignons aux algorithmes fonctionnant par tours et nous utilisons le modèle Heard-Of qui abstrait les défaillances en représentant par un prédicat l’ensemble des pairs pour lesquels un pair donné reçoit un message à un tour donné. Nous avons apporté des réponses à deux questions alors ouvertes : comment trouver le prédicat heard-of qui correspond à un modèle classique donné ? quelles pertes surviennent lors de cette conversion ? Une formalisation de la dérivation d’un prédicat heard-of correspondant à un certain modèle, avec une méthodologie pour dériver un modèle à partir de modèles plus simples, permet de répondre à la première question. La seconde question a été résolue grâce à une équivalence entre des prédicats heard-of et les modèles à messages asynchrones avec détecteurs de défaillances.

Vos propositions sont les bienvenues !

Séminaire autour des thèmes 68NQRT