The Oasis team develops methods and tools for the analysis and the verification of
applications built from distributed components. A central piece in these activities is
the "model-checker", that checks whether a property is true in all possible states
of the application behaviour. We currently use "classical" model-checkers, that are based on
the explicite or symbolic enumeration of a finite state-space.
Independantly, several french research teams are working on the development of methods
for the model-checking of infinite state-spaces, when this state-space has a regular
structure (e.g. generated by stacks, fifos, or similar structures).
During this Research Master we plan to explore the possibilities of using this kind of new
methods in our specific application domain.
After a review of the current state of model-checking tools available, and in particular those offered by the PERSEE action (Altarica language and tool, Fast and TRex tools), the student will explore, using concrete Proactive case-studies, the possibility of using those tools. He/she will develop software connections between Oasis analysis tools and Persee model-checkers.
The research takes place in Sophia Antipolis, within the OASIS research team, a joint project between INRIA, CNRS-I3S, and University of Nice Sophia Antipolis.
Internship location:
The research takes place in Sophia Antipolis, within the OASIS research
team, a joint project between INRIA, CNRS-I3S, and University of Nice
Sophia Antipolis.
Director: Eric Madelaine
Phone: 04 92 38 78 07
email: eric.madelaine@sophia.inria.fr