Activities area

The COSMO (COmmunications Spécifications Models) team studies the fundamental properties of computer and biological systems and, more generally, the behavior of reactive, decentralized and open dynamic systems. Within this framework, it is concerned with the specification and analysis of these systems, as well as with their design. The team is characterized by continuity between fundamental and applied research, with significant theoretical advances, methodological developments, the production of software tools, applications to real-life problems, and the creation of industrial links. The team’s research is structured along two lines.

  1. An applicative approach focused on societal problems (personalized medicine, vehicles of the future, Internet of the future, etc.) for which new theoretical or methodological frameworks need to be defined.
  2. Work rooted in a “core competency” theory that may have spin-offs in the first direction and find their application there. This dual orientation favors the production of software and methodological tools, both to enable application and as a validation of the theory.

Keywords :

formal modeling and analysis, proof, Petri nets, process algebras, Boolean networks, automata networks, modal logic, array methods, entity-centered simulation, precision personalized medicine, communicating autonomous vehicles, systems biology, Internet of future, autonomic networks, multi-agents

Application areas

In the area of personalized and precision medicine, one of the main goals is the design of decision support software for diagnosis and therapy. In this perspective, the main challenge is the lack of methods to interpret the data of the “omic”. Focusing on the prediction of therapeutic targets based on the analysis of molecular networks, we formalized adapted theoretical frameworks in order to infer the causal targets responsible for phenotypic transition (healthy / sick). Our methodology is implemented in a set of software tools based on game theory and abduction principles applied to Boolean networks.

We also worked on the modeling, simulation and formal verification of decision modules of autonomous and communicating vehicles. We have proposed in this framework an original, scalable and parametric modeling in timed automata and also a modeling of multi-agent simulation, both of which make it possible to evaluate the aspects of security, fluidity and comfort of various decision policies. We have shown in particular, by developing a comparison between these two approaches, what impact the level of abstraction chosen on the indicators considered had. Our simulation method has been implemented in a plugin for the Gama simulator.

We are also interested in Cloud Computing and IoT (Internet of Things) technologies in the context of the Internet of the Future. The deployment of these technologies involves many problems of great complexity. We then proposed several approaches to the modeling of these problems in order to relax some constraints by a better understanding of the specificities of these technologies and their use. We also addressed the problem of holistic and autonomic control of a converging “Cloud IoT” environment meeting the time and processing resource requirements for collecting data from thousands of potentially deployed sensors in the environment. Finally, we proposed a modeling based on Petri nets autonomic mechanisms to manage the elasticity of resources in the Cloud, whose analysis was conducted using our SNAKES tool.

Other applications were studied. In particular we proposed a formal framework for modeling and analysis of distributed storage systems, for example cache hierarchies in high performance computing architectures in collaboration with the CEA. More recently, a collaboration with INRA Montpellier has started on ecosystem modeling and analysis.

 

Last deposits

Chargement de la page

Full-text documents

223

Open Access documents %

60 %

Bibliographical references

230

Keywords

Modal logic Abstraction Cloud of Things Computer science AMC Knowledge representation Resource Allocation Security protocols Artificial intelligence Detection algorithm BPEL Elasticity Control sequence Trust Biological regulation networks Semantics Model-checking Satisfiability 3GPP Provisioning QoS Attractor Convergence time Abductive reasoning Blockchain Deadlocks Complex networks IoT Automata networks Scheduling P systems Bisimulation Verification Resources Allocation Ecosystems Cloud Computing Cloud RAN Compilation Service Level Agreements Alternating-time temporal logic Autonomous vehicles Context data Reachability Context management Simulation Cloud computing 5G networks Abduction Complex Network Discrete dynamical systems Internet of Things Tableaux Asymptotic behaviour Game theory Communicating Autonomous Vehicles Boolean network BSP Compositional translation Biological networks CTL 5G Security Biological network modelling Optimization Pattern matching Petri nets Design science research Model compilation Drug target prediction Agent-based simulation Cycles ATL SLA Model checking Data reduction Timed automata Boolean Network Community structure Boolean automata networks Complexity Cloud RRH Synthetic biology Box algebra Automated theorem prover Context-awareness Computational completeness Explicit model-checking Interaction networks Composition Boolean control network Derivation modes Context-aware Hybrid logic Timed Automata Boolean networks Automated reasoning Formal modelling Mobility Systems biology Offloading