LMF
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Test Club meeting on December 18 2017

Personnes présentes

  • Dominique Marcadet
  • Safouan Taha
  • Frederic Boulanger
  • Frederic Voisin
  • Hai Nguyen Van
  • Boutheina Bannour (CEA LIST/LISE)
  • Marie-Claude Gaudel
  • Chantal Keller
  • Thibault Balabonski
  • Delphine Longuet

ODJ

  • Tour de table
  • Discussion des thèmes
  • Choix: Travaux de thèse de Hai sur TESL
  • Courte discussion sur des invités pour le séminaire VALS

Current Theme List

  • Diversity + demo
  • Extension Test Elimination Chemin Faisable
  • Invariant Generation in Kind2 and PDR
  • Testing an Odometer Component

Testing in TESL : An Introduction

Presentateur: Hai Nguyen Van

TESL is a kind of "timed choreography language" for interacting subcomponents.

TESL assumes the ability to observe communications (ticks) at the interfaces of subcomponents, which are tagged with a timestamp of the local time of this subcomponent (the tag for short). An observation point at an interface is called a clock. Local time in a subcomponent is assumed to pass monotonically (time elapses).

A run is a possible causal sequence of observed tick, but note that local time evolves independently of an observation.

The TESL language provides a number of operators that allow to specify sets of runs in a TESL judgement.

In order to handle the infinite number of runs, we introduced the concept of a symbolic run, a FOL-formula based on some elementary predicates.

A denotational semantics is introduced that specifies the sets of runs of each operator; juxtaposition of TESL judgements corresponds to the intersection of the underlying run sets.

The operational semantics allows for constructing symbolic runs.

The operational semantics is proven to be sound and complete wrt. the denotational one.

The operational semantics can be used for monitoring and testing and has been implemented in a tool called Heron (https://github.com/heron-solver/heron).