About MExICo
A joint team with
Permanent Members | ||
| Benedikt Bollig Researcher, CNRS | Paul Gastin Professor, ENS Cachan | Serge Haddad Professor, ENS Cachan |
| Thomas Chatain Assistant professor, ENS Cachan | Stefan Haar Senior researcher, INRIA | Stefan Schwoon Assistant professor, ENS Cachan (INRIA chair) |
Associated and Temporary Members | ||
| Clément Démoulins Engineer, CNRS | ||
Ph.D. Students | ||
| Sandie Balaguer PhD student, INRIA et ENS Cachan | Hilal Djafri PhD student, ENS Cachan | César Rodríguez PhD student |
| Benoît Barbot PhD student, ENS Cachan | Benjamin Monmege PhD student, ENS Cachan | |
| Aiswarya Cyriac PhD student, Digiteo and ENS Cachan | Hernan Ponce de Leon PhD student | |
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 works towards a better understanding and an increased reliability of distributed and asynchronous systems, and focusses its research on the two features of Concurrency and Interaction. The increasing size and the networked nature of communication systems, controls, distributed services et.c 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.
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.
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).
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:
A joint team with
| • | . Effective Verification of Weak Diagnosability. In SAFEPROCESS'12. IFAC, 2012. To appear. ( PDF | BibTeX ) |
| • | . Importance Sampling for Model Checking of Continuous-Time Markov Chains. Research Report LSV-12-08, Laboratoire Spécification et Vérification, ENS Cachan, France, 2012. 15 pages. ( PDF | BibTeX ) |
| • | . Frequency Linear-time Temporal Logic. In TASE'12. IEEE Computer Society Press, 2012. To appear. ( PDF | BibTeX ) |
| • | . Refinement and Asynchronous Composition of Modal Petri Nets. In Transactions on Petri Nets and Other Models of Concurrency V, LNCS 6900, pages 96-120. Springer, 2012. ( PDF | BibTeX ) |
| • | . A Concurrency-Preserving Translation from Time Petri Nets to Networks of Timed Automata. Formal Methods in System Design, 2012. To appear. ( PDF | BibTeX ) |