LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on October 7 2015

Personnes présentes

  • Romain Aissat
  • Thibaut Balabonski
  • Frédéric Boulanger
  • Chantal Keller
  • Yakoub Nemouchi
  • Safouan Taha
  • Frédéric Tuong
  • Freek Verbeek
  • Burkhart Wolff

Project

Thibaut

Generation of traces for concurrent systems. Interleaving of threads (sequences of operations). Reduction of the number of possible traces by grouping traces that have the same behavior (normalization by reordering some operations in a trace).

Some operations interfere and cannot be permuted without changing the behavior. We want to normalize traces by permuting non interfering operations in traces.

An order {$\prec$} is used to define a standard form for reordered traces.

The standardization algorithm (kind of selection sort) if proven to preserve the order of interfering elements.

The ultimate goal is to show that testing the conformance of a system to a specification according to all interleavings is the same as testing the conformance of the system to the specification according to interleavings that respect the order.

Previous meeting -- Next meeting