[ecoop-info] Postdoc Position on Formal Verification of Model-based Software Design, INRIA Grenoble, France

[Gwen.Salaun at inria.fr]

-----------------------------------------------------------------
Post-doctoral position for 12 months at INRIA Grenoble (France)
-----------------------------------------------------------------
 
Title: Formal Analysis and Verification of Model-based Software Design
 
Description: Recent computing trends promote the development of
software applications that are intrinsically both parallel and
distributed. Here are a few examples:

· Embedded systems that involve many components such as controllers,
sensors, processors, etc., which interact to fulfill some specific
functions.

· Software and middleware technologies that connect smart grids and
smart meters in order to anticipate and optimize energy consumption.

· Service-oriented computing that enables implementation of
Web-accessible software systems that are composed of distributed
services, which interact with each other by exchanging messages.

· Cloud computing that leverages hosting platforms based on
virtualization, and promises to deliver computational resources on
demand via a computer network.
 
However, designing and developing distributed software has always been
a tedious and error-prone task, in particular because software is
becoming more and more complex. In this context, choreography modeling
languages have recently been proposed for specifying and designing
software applications involving interacting entities (components,
services, etc.) from a global perspective. These languages enable us
to design the system from a centralized point of view, although the
corresponding application will behave in a fully parallel fashion. So
far, several formalisms have been proposed, such as WS-CDL, UML
collaboration diagrams, BPEL4Chor, BPMN 2.0 choreographies, process
calculi (e.g., Chor), Petri nets, conversation protocols, etc. The
main advantage of choreography-based system design is that it is
possible from such global models to derive a distributed
implementation of the application, which behaves exactly as specified
in the choreography specification. This is known as realizability or
enforceability, and ensures the correct-by-construction design of the
distributed application.
 
However, although the number of specification languages has increased
surprisingly quickly in recent years, there are still many open issues
that deserve to be studied and resolved. The goal of this
post-doctoral position is to apply and extend existing formal
techniques and tools in order to resolve these issues. The work plan
of this post-doctoral position will consist first in studying some
fundamental aspects, and proposing solutions to these issues. In a
second step, these ideas will be validated through implementation and
experiments.
 
Requirements: Candidates should be fluent in English. Experience in
formal methods (e.g., process calculi, model checking tools, etc.) is
recommended. Knowledge in modeling languages (e.g., UML,
workflow-based notations, etc.) is an advantage but is not
necessary. Candidates who enjoy programming would be appreciated, as
the work is likely to include software development.

Application: Candidates should send a short resume via email to
Gwen.Salaun at inria.fr.  Applications should be sent by September 1,
2011, and the selected applicant will start by the end of November
2011. Gross salary is about 2,600 euros per month.
 
Contact: Gwen Salaün
Email: Gwen.Salaun at inria.fr
Webpage: http://www.inrialpes.fr/vasy/people/Gwen.Salaun/