[ecoop-info] Post-doctorate position at Supélec

[Cécile Hardebolle]

Post-doctorate position at Supélec
----------------------------------
The Computer Science Department of Supélec is seeking a post-doctorate
candidate for a one year position.
The topic of the post-doctorate is to define an architecture description
language targeted to the integration of control and data-processing in
applications. The control part will generally be specified using state
machines or synchronous reactive modules while the data processing part will
be modeled by a data-flow network. The topology of this network is modified
according to the behavior of the control part when the application is
running. The precise models of computation used for control and for
data-processing are specified in the description of the application, and
must be taken into account to determine the global behavior of the system.

Using this language to describe a system should make it possible to generate
an implementation of the system by assembling the code of the control part
and of the data-processing part. It should also allow the transformation of
properties of the whole system into properties that can be verified on the
control part using model-checking tools. The fact that the same description
of the system is used to generate implementations and to transform the
properties improves the consistency between the property that is verified
and the effective property of the real system.

Location: Supélec, 91192 Gif-sur-Yvette, France
Date: as soon as possible.
Duration: 1 year
Contact: Yolaine Bourda
          +33 [0]1 69 85 14 80
          Yolaine.Bourda at supelec.fr
Profile:
   - PhD obtained before December 31 2006
   - good knowledge of model driven engineering and
     heterogeneous modeling
   - knowledge of usual models of computation for control (state
     machines, synchronous reactive systems) and data-processing
     (static and dynamic data-flow models), as well as how they
     can be implemented in software
   - solid background in formal verification of properties.

=========

Supélec recrute un post-doctorant
---------------------------------
Le Département Informatique de Supélec recrute un post-doctorant pour un
contrat d'un an. L'objet de la recherche est la définition d'un langage de
description d'architectures logicielles permettant d'intégrer le contrôle et
les traitements. Typiquement, le contrôle sera spécifié sous forme
d'automates ou de modules réactifs synchrones, tandis que les traitements
seront modélisés par des réseaux d'opérateurs à flots de données. La
topologie de ce réseau est modifiée par le contrôle au cours du
fonctionnement du système. Les modèles de calcul utilisés pour le contrôle
et pour les traitements sont indiqués dans la description de l'application
et doivent être pris en compte pour déterminer le comportement du système.

À partir de la description de l'architecture d'un système dans ce langage,
on souhaite pouvoir générer une implémentation du système par assemblage du
code du contrôle et du code des traitements. On souhaite aussi pouvoir
exprimer des propriétés sur le système et les transformer automatiquement en
propriétés vérifiables sur le contrôle par des outils de model-checking. Le
fait que le même langage serve à générer l'implémentation du système et à
transformer des propriétés à vérifier permet d'assurer la cohérence entre la
propriété valide dans le modèle et sa contrepartie dans le système.

Lieu : Supélec, 91192 Gif-sur-Yvette
Date : aussitôt que possible.
Durée : 1 an.
Contact: Yolaine Bourda
          +33 [0]1 69 85 14 80
          Yolaine.Bourda at supelec.fr

Profil recherché : Titulaire d'un doctorat soutenu avant le
31 décembre 2006, le candidat doit :

   - posséder une bonne culture en matière d'ingénierie dirigée
     par les modèles et de la modélisation hétérogène
   - connaître les modèles de calcul utilisés pour la spécification
     du contrôle (automates, systèmes réactifs sychrones) et des
     traitements (modèles à flots de données statiques ou dynamiques)
     ainsi que les techniques d'implémentation de ces modèles

   - maîtriser les concepts de base de la vérification formelle
     de propriétés d'un système.