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

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