MEXICO: Modelling and Exploitation of Interaction and Concurrency

Research Topics

In the increasingly networked world, reliablity of applications becomes ever more critical as the number of users of, e.g., communication systems, web services, transportation etc grows steadily. MExICo will work towards a better understanding and an increased reliability of distributed and asynchronous systems, and thus join the existing effort of many other teams that use formal methods; what is particular in the present proposal is that our team focusses its research on the two features of concurrency and interaction.


Permanent Members

Thomas Chatain
Assistant professor, ENS Cachan
Stefan Haar
Senior researcher, INRIA Saclay-Île de France
Stefan Schwoon
Assistant professor, ENS Cachan
Matthias Függer
Researcher, CNRS
Serge Haddad
Professor, ENS Cachan
Laurent Fribourg
Senior researcher, CNRS
Claudine Picaronny
Assistant professor, ENS Cachan

Associated and Temporary Members

Béatrice Bérard
Resarcher, INRIA (professor, University Paris 6)
Adrien Le Coënt
PhD student at CMLA

Ph.D. Students

Yann Duplouy
PhD student, IRT SystemX
Engel Lefaucheux
PhD student, ENS Cachan (joint with IRISA, Rennes)
Adnane Saoud
PhD student, Digicosme project Emergence CODECSYS (joint with L2S)
Juraj Kolcak
PhD student, ANR-FNR AlgoReCell
Tymofii Prokopenko
PhD student (joint with Polytechnique)

Detailed Presentation

The increasing size and the networked nature of communication systems, controls, distributed services etc. confront us with an ever higher degree of parallelism between local processes. For any form of analysis and control, a global view of the system state leads to overwhelming numbers of states and transitions, and blurs the mechanics that are at work rather than exhibiting them. Conversely, respecting concurrency relations avoids exhaustive enumeration of interleavings, and allows to focus on 'essential' properties of nonsequential processes characterized by causal precedence relations. We see concurrency in distributed systems as an opportunity rather than a nuisance that leads to state space explosion in the formal models and slows down algorithms.

Diagnosis and Diagnosability

In diagnosis for discrete event systems, the task is to determine - from observations of streams of event labels - whether faults have occured in the system under observation. Diagnosis algorithms have to operate in contexts with low observability, i.e., in systems that exhibit many events invisible to the supervisor. Checking observability and diagnosability for the supervised systems is therefore a crucial and non-trivial task in its own right. MExICo works on the following aspects:


Let a formal specification model M and an implementation I, that supposedly conforms to M, be given; I's behaviour is influenced by the input streams received, and observable only via an output stream. Conformance testing consists in computing - whenever possible - input streams that allow to determine whether I deviates from M or conforms to it. MExICo's research is on testing for distributed asynchronous systems.

Dynamic and Parameterized Communicating Systems

Many distributed programs do not depend on a fixed network topology, but shall be run on arbitrary architectures such as star topologies, bus topologies, trees, grids, or rings. They may also generate their communication topology dynamically at runtime. We aim for high-level specification formalisms and automata models that support the synthesis and formal verification of such systems.

Controler Synthesis

In a distributed setting, we need to synthesize a distributed program or distributed controllers that interact locally with the system components. The main difficulty comes from the fact that the local controllers/programs have only a partial view of the entire system. It is essential to specify expected properties directly in terms of causality revealed by partial order models of executions (MSCs or Mazurkiewicz traces).

Adaptation and Grey Box Management

Contrary to mainframe systems or monolithic applications of the past, we are experiencing and using an increasing number of services that are performed not by one provider but rather by the interaction and cooperation of many specialized components. As these components come from different providers, one can no longer assume all of their internal technologies to be known (as it is the case with proprietary technology). Thus, in order to compose e.g. orchestrated web services, to determine violations of specifications or contracts, to adapt existing services to new situations etc, we have to analyze the interaction behaviour of components known only through their public interfaces, thus semi-transparent and semi-opaque; we refer to them as "grey boxes". Three central issues emerge:

National and International Collaborations

Ongoing projects

Past projects:

About LSV

About MExICo

A joint team with

Logo INRIA Saclay

Presentation of MExICo (2013)

Mexico presentation at AERES (2013)

Vasco-Mexico seminar

No entries.

Recent Publications

All the MEXICO publications

S. Haar, S. Perchy and F. ValenciaD-SPACES: Implementing Declarative Semantics for Spatially Structured InformationIn ICSC'17, IEEE ICSC 11. IEEE Press, January 2017. Web page | PDF | BibTeX )
M. Guzman, S. Haar, S. Perchy, C. Rueda and F. ValenciaBelief, Knowledge, Lies and Other Utterances in an Algebra for Space and Extrusion 86(1), pages 107-133, 2017. Web page | PDF | BibTeX )
B. van Dongen, J. Carmona, Th. Chatain and F. TaymouriAligning Modeled and Observed Behavior: A Compromise Between Complexity and QualityIn CAiSE'17, LNCS 10253. Springer, June 2017. To appear. PDF | BibTeX )
B. Barbot, B. Bérard, Y. Duplouy and S. HaddadStatistical Model-Checking for Autonomous Vehicle Safety ValidationIn SIA Simulation Numérique. March 2017. Web page | PDF | BibTeX )
B. Bérard, S. Haar, S. Schmitz and S. SchwoonThe Complexity of Diagnosability and Opacity Verification for Petri NetsIn PETRI NETS'17, LNCS 10258, pages 200-220. Springer, June 2017. Web page | BibTeX )

All the MEXICO publications