----------------------------------------------------------------- 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 [email protected]. 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: [email protected] Webpage: http://www.inrialpes.fr/vasy/people/Gwen.Salaun/
---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
