Pause
Lecture
Moteur de recherche d'offres d'emploi CEA

Heuristics and reduction techniques for the analysis of models of distributed systems H/F


Détail de l'offre

Informations générales

Entité de rattachement

Le Commissariat à l'énergie atomique et aux énergies alternatives (CEA) est un organisme public de recherche.

Acteur majeur de la recherche, du développement et de l'innovation, le CEA intervient dans le cadre de ses quatre missions :
. la défense et la sécurité
. l'énergie nucléaire (fission et fusion)
. la recherche technologique pour l'industrie
. la recherche fondamentale (sciences de la matière et sciences de la vie).

Avec ses 16000 salariés -techniciens, ingénieurs, chercheurs, et personnel en soutien à la recherche- le CEA participe à de nombreux projets de collaboration aux côtés de ses partenaires académiques et industriels.  

Référence

2021-18949  

Description de l'unité

Within the CEA, the LECS is a 15-person team working on system modeling, system requirements engineering and formal analysis and conformance of systems. These activities are conducted with objective to ensure high levels of confidence on system safety and security and demonstrate their compliance with reference standards. The team contribute to the open source platforms hosted by the Eclipse platform, namely Formal Modeling https://projects.eclipse.org/projects/modeling.efm and Papyrus https://www.eclipse.org/papyrus/.

Description du poste

Domaine

Mathématiques, information  scientifique, logiciel

Contrat

Stage

Intitulé de l'offre

Heuristics and reduction techniques for the analysis of models of distributed systems H/F

Sujet de stage

The objective of the internship is to develop heuristic algorithms for the exploration of distributed system models.

Durée du contrat (en mois)

6

Description de l'offre

The use of formal methods classically consists of assessing the correctness of a system against a model (or properties) characterizing the expected behaviors of the system, using logic-based algorithms. In order to benefit from the high level of confidence offered by these approaches, a key factor is to have a high level of confidence in the model itself. Such a model must describe the intended behaviors of the system as closely as possible. Achieving this level of confidence is difficult for distributed systems due to the asynchronous message exchanges and the varying times taken to route these messages.  Indeed, as there is no global clock to order the events occurring on different subsystems, several orders of these events can be observed. Distributed systems are composed of subsystems deployed on different computers and interconnected via a communication medium.  In order to reflect these features, distributed systems are often modeled as a collection of subsystem models, structured with communicating operators that help mimic the highly asynchronous behaviors of the existing system. In such a context, even if each subsystem model is well understood, the behaviors characterized by the structuring of these models via communication operators are often challenging to predict by the modeler. In such a context, having techniques to explore possible behaviors characterized by distributed system models is an essential asset.

The objective will be to propose reachability algorithms for distributed system models, which explore the model behaviors guided by a particular user coverage objective. In order to deal with the combinatorial of the many possible re-orderings of the distributed events, these algorithms will be heuristic-based and potentially apply on-the fly reduction techniques.  

These issues are related to an existing tooled formalism at CEA dedicated to the symbolic execution of distributed system models, within a paradigm of communicating symbolic automata. Intuitively, a distributed system model is composed of a collection of automata (one for each subsystem) connected through ports. The symbolic execution framework takes into account the asynchronous nature of communications by allowing any delay between the emission and receiving of a given message. In addition, our models deal with real-time constraints using formulas on particular variables called clocks and time constraints local to the subsystems.

 

Profil du candidat

Candidates should have a clear background in Computer Science with excellent programming skills. Knowledge in formal methods, automata paradigm or symbolic execution will be appreciated.

Localisation du poste

Site

Autre

Localisation du poste

France, Ile-de-France, Essonne (91)

Ville

Palaiseau (site de Nano Innov)

Critères candidat

Langues

Anglais (Courant)