PhD Position F/M Formal Modelling and Automated Analysis of Resource Provisioning Languages

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.

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.

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.

# 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
 

• 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

• 1st year: 2082 euros gross salary
• 2nd & 3rd years: 2191 euros gross salary