MEXICO Research team
Modeling and Exploitation of Interaction and Concurrency
- Leader : Stefan Haar
- Type : Project team
- Research center(s) : Saclay
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Proofs and Verification
- Partner(s) : CNRS,Ecole normale supérieure de Cachan
- Collaborator(s) : Laboratoire specification et vérification (LSV) (UMR8643)
In the increasingly networked world, reliability 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 focuses 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.
The MEXICO team works on complex and concurrent systems from both a theoretical and practical point of view.
Our work is driven by applications in two fields, namely Cyber-physical systems and
Biological systems, and by the methodological challenges posed on the abstract level in the context of i)
hybrid/timed/asynchronous systems, ii) distribution and concurrency, and iii) partially observable systems.
Application 1 : Cyber-physical systems (CPS)
CPS are organized as networks of digital components which, on the one hand, analyze
information flows coming via sensors from the environment, and on the other hand, react by controlling
actuators. The efficient management of these flows raises in particular the problems of choosing an architecture and setting clock frequencies.
We have attacked this problem by weakening the classical untimed Boolean abstraction of circuits, and
treat them as timed hybrid systems with analog effects. Our goals include
- a more accurate prediction for timing and power consumption, and thus reduced conservative frequency and power margins.
- enable formal verification of circuits, meeting solvability boundaries of classical problems, such as on the short
pulse filtration problem.
Applications include autonomous transportation systems, in particular collision avoidance for
Biological systems I: (Re-)programming in discrete concurrent models
Cellular regulatory networks exhibit highly complex
concurrent behaviours that is influenced by a high number of perturbations such as mutations. We are in particular
investigating discrete models, both in the form of boolean networks and of Petri nets, to harness this
complexity, and to obtain viable methods for two interconnected and central challenges:
• find attractors, i.e. long-run stable states or sets of states, that indicate possible phenotypes of the
organism under study, and
• determine reprogramming strategies that apply perturbations in such a way as to steer the
cell’s long-run behaviour into some desired phenotype, or away from an undesired one.
II : Distributed Algorithms in wild or synthetic biological systems We also work, on the multi-cell level, with
distributed algorithms’ view on microbiological systems, both with the goal to model and analyze existing
microbiological systems as distributed systems, and to design and implement distributed algorithms in
synthesized microbiological systems. Major long-term goals are drug production and medical treatment via synthesized bacterial colonies.
Research topic A: Systems continuous in state and time
We study modeling,
controller synthesis, and verification for systems that are continuous in state, time, or both. In particular, this includes -“periodic switched
systems”, governed by a finite number of modes, corresponding to
specific dynamics whose change of mode occurs periodically in time.;
- used hybrid system models as abstraction for differential equations, e.g. describing signal traces of
digital gates, to enable
verification of high-speed digital circuits;
- Continuous state Continuous Petri nets (CPN)
Research topic B:
Distributed and concurrent systems
The analysis of discrete event systems is one of the central activities of the team. We investigated several topics concerning
concurrent systems and distributed algorithms.
Unfoldings The study of the partial order semantics of Petri nets and related models has brought results
on diverse applications, and on the theory in its own
right, such as for reset nets, summaries [CI-241], reveals relations, and goal-driven
unfoldings; this is one of our key approaches.
Distributed Algorithms: We consider distributed algorithms for dynamic communication
networks to solve agreement problems. These algorithms occur as building blocks in distributed control
applications, such as distributed clock synchronization. One major topic of research is metastability-
tolerant circuits; it has applications in high-speed control circuits and fault-tolerant dis-
tributed algorithm implementations.
Research topic C: Partially observable systems
In many systems, one or several observers can
see only parts of the execution, and strive to gain knowledge about the system state. The observers may be
- friendly (performing diagnosis or testing) or hostile (trying to infer secrets), in which case the designer wants
to make the system opaque), and
- be passive or active, i.e. help the
system to either avoid or diagnose faults;
the systems under observation may be of different nature, e.g.
sequential/concurrent, non-deterministic, or probabilistic, opening also variants of exact and accurate diagnosis, as well as.
When no complete model of the underlying dynamic system is available, the analysis
of logs may allow to reconstruct such a model, or at least to infer some properties of interest; this activity,
which has emerged over the past 10 years on the international level, is referred to as process mining. We
have studied unfolding-based unfolding-based process discovery , and the study of process alignments, and continue to work on these fields under the particular angle of concurrent systems.
MINIMATOR, a tool for control
synthesis in cyberphysical systems.
Cosmos (http://cosmos.lacl.fr/) is a statistical model checker for Hybrid Automata Stochastic Logic. It evaluates such formulas on a Discrete Event Stochastic Process (DESP), a class of stochastic
models which includes, but is not limited to, Markov chains. As a result, HASL verification turns out to be a
unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-
based analysis. Cosmos is written in C++ and is freely available to the research community.
MINIMATOR (https://bitbucket.org/ukuehne/minimator/overview) allows to synthesize automatically a
control for cyberphysical systems that satisfies desired properties of safety and stability. MINIMATOR has been
successfully applied to real case studies such as power electronics devices and smart heating of an
11-room building in Denmark.
International and industrial relations
- Strong links and exchanges with
- ANR project AlgoReCell on Computational Models and Algorithms for the Prediction of Cell Reprogramming Determinants with High Efficiency and High Fidelity, ANR-FNR project 2017-2020, with LRI BioInfo group; Institut Curie, Computational Systems Biology of Cancer group; and University of Luxemburg, FSTC and LCSB.
- ANR project Checkbound with LACL, LAMSADE, LIG, LSV, INT, PRISM on model checking for performability and security of computer systems.
- INRIA associate team LifeForm with University of Newcastle (UK) and Leiden University (NL)
- Several other academic cooperations with Chennai Mathematical Institute (CMI), India, Polytech of Catalunya, Leipzig, Duisburg, Padova, Bordeaux, Milan etc.al
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CELTIQUE - Software certification with semantic analysis
- CONVECS - Construction of verified concurrent systems
- DEDUCTEAM - DEDUCTEAM
- GALLINETTE - Gallinette: developing a new generation of proof assistants
- GALLIUM - Programming languages, types, compilation and proofs
- MARELLE - Mathematical, Reasoning and Software
- MOCQUA - Designing the Future of Computational Models
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- SUMO - SUpervision of large MOdular and distributed systems
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems