Tools related to project or publications


COnfECt is a model inference approach that takes execution traces of a component based system and infers LTSs (Labelled Transition Systems) for each component of the system. It is based on kTail, a passive model learning method that works in two steps:

  1. First, it constructs a tree from the traces, with each branch of the tree corresponding to a trace, and each event to an edge.
  2. Then, it merges all states of this tree that have the same k-future, i.e. the states that have the same future of length k.

The method COnfECt adds two steps to kTail: Trace Analysis & Extraction, and LTS synchronisation.

Git link

Model generation

Model generation


TFormat is a trace formatting tool. It takes raw messages, sorts out them, transforms them in actions (that can be read by COnfECt), and builds execution traces.

Git link


Model reverse engineering of Android applications

Feature: * models generation, storyboard generation, * security vulnerability detection : SQL injection, brute force, * crash detection, etc.

wiki link Git link

Storyboard example


Model generation

Model generation


an Android aPplication SEcurity Testing tool for detecting intent-based vulnerabilities.

Git link

Cloud PASTE (Cloud PASsive TEsting)

Cloud PASTE is tool for passively testing Web service compositions deployed in PaaS platforms. At the moment, we provide a version of the tool for Google AppEngine (GAE) only. This passive tester takes a specification described with ioSTSs expressing the functional behaviours of the composition and tests its implementation deployed in GAE.

This passive tester is based upon the notion of transparent proxy for testing. Classical tools for monitoring/passive testing cannot be used with Clouds since the Cloud architecture restricts the access and prevent from installing a classical test architecture (sniffer based tool etc.). So, we derive a model called proxy-tester for testing.

Cloud PASTE page here

Passive tester architecture:


Tester interface:


Black box web service testing WS-AT

WS-AT (Web Service Automatic Test tool) : Random test case generation with random values and predefined values well known for relieving bugs.

A dedicated page for WS-AT, showing its functionning can be found here.

Features: * Kind of tests : operation existance, robustness, session

Tester interface:



Some results:


And a video :

Test case generation from timed automata and region graphs

Test case generation with the State characterization method. Test case generation with a parallel algorithm using OPENMP

Example with a Timed automaton (part of the GSM protocol):


The associated region graph :

Region graph

State Caracterization results (complete results here

test cases

Ajax components automatic testing



The tester:


A video showing some tests: