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:
- First, it constructs a tree from the traces, with each branch of the tree corresponding to a trace, and each event to an edge.
- 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.
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.
Model reverse engineering of Android applications
Feature: * models generation, storyboard generation, * security vulnerability detection : SQL injection, brute force, * crash detection, etc.
Storyboard example Model generation
an Android aPplication SEcurity Testing tool for detecting intent-based vulnerabilities.
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.
Passive tester architecture:
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
- provided with a classical interface or with an Eclipse pluggin.
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 :
State Caracterization results (complete results here
Ajax components automatic testing
- Test case generation using random values and predefined values known for relieving bugs. * Test architecture implementation.
- Tool for modeling Ajax components with UML sequence diagrams.
A video showing some tests: