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.