PhD Position F/M Formal Modelling and Automated Analysis of Resource Provisioning Languages
Type de contrat : CDD
Niveau de diplôme exigé : Bac + 5 ou équivalent
Fonction : Doctorant
Niveau d'expérience souhaité : Jeune diplômé
A propos du centre ou de la direction fonctionnelle
The Centre Inria de l’Université de Grenoble groups together almost 600 people in 22 research teams and 7 research support departments.
Staff is present on three campuses in Grenoble, in close collaboration with other research and higher education institutions (Université Grenoble Alpes, CNRS, CEA, INRAE, …), but also with key economic players in the area.
The Centre Inria de l’Université Grenoble Alpes is active in the fields of high-performance computing, verification and embedded systems, modeling of the environment at multiple levels, and data science and artificial intelligence. The center is a top-level scientific institute with an extensive network of international collaborations in Europe and the rest of the world.
Contexte et atouts du poste
Mission confiée
Resource provisioning languages (such as TOSCA) allow one to model resource
properties and dependencies for distributed applications (for instance components interacting
via a network and hosting software), but also to automate provisioning, deployment
and instantiation of these resources. The resource provisioning languages
provide support to the Infrastructure as Code (IaC) approach, which is widely
present in the industry. These languages can also be considered as architecture
description languages (ADL). The IaC approach is particularly popular and used
in cloud computing in order to avoid manual tasks and thus automate as much as
possible the deployment and update of applications based on services available
in the cloud.
Principales activités
The first objective of this PhD Thesis is to extend and improve resource
provisioning languages in terms of expressiveness while providing a formal semantics
to them. The plan is to study existing resource provisioning languages (including TOSCA),
in order to evaluate them in terms of expressiveness and precisely identify the
application lifecycles allowed by these languages. This study could lead to
the definition of a new Domain Specific Language expressive enough to represent
complex orchestration operators and model specific lifecycles. This new
language will be equipped with a formal semantics so as to avoid ambiguity and
simplify its further analysis.
The second objective of this PhD Thesis is to develop automated analysis
techniques to verify behavioural and quantitative properties that must respect
the applications deployed using the aforementioned languages. Several functional
properties have already been identified for resource provisioning languages.
To analyze these properties, a possible solution is to rely on model checking techniques.
The verification of quantitative properties is also planned, particularly
deployment times and costs but also the detection of undesired delays that could be
avoided during the deployment or reconfiguration of a cloud application.
All the contributions made during this PhD Thesis will be validated via
prototype tools and applied on realistic case studies.
Compétences
# Required skills and profile:
- Knowledge of cloud computing and information/data models is welcome
- Knowledge of formal methods (concurrency theory) and verification is a plus
- Candidates who enjoy programming would be appreciated, as the work will include software development
- Education: MSc/Master 2 Recherche in Computer Science
- Good command of English as the working language, French is a plus
Avantages
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
Rémunération
- 1st year: 2082 euros gross salary
- 2nd & 3rd years: 2191 euros gross salary
Informations générales
- Thème/Domaine :
Systèmes distribués et intergiciels
Systèmes d'information (BAP E) - Ville : Montbonnot
- Centre Inria : Centre Inria de l'Université Grenoble Alpes
- Date de prise de fonction souhaitée : 2024-10-01
- Durée de contrat : 3 ans
- Date limite pour postuler : 2024-06-30
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : CONVECS
-
Directeur de thèse :
Salaün Gwen / gwen.salaun@inria.fr
L'essentiel pour réussir
- Proven communication and interpersonal relationship skills, attention to detail, methodical approach, autonomy, team player
A propos d'Inria
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.