============================================================================
Post-doctoral position
LSR Laboratory IMAG
Grenoble France
============================================================================
A post-doctoral position will be available from september 2001 at the
LSR (Logiciels, Systèmes, Réseaux - Software, Systems, Networks) Laboratory
in Grenoble, to carry out research within a RNTL project. RNTL means
"Réseau National des Technologies du Logiciel" - "National Network on
Software Technologies" and has been set up by the french Ministry of
Industry in 2000.
Salary Range: 1840 Euros/month.
For any information, please contact:
Didier Bert EMail: [log in to unmask]
LSR-IMAG Phone: +33 476 82 72 16
BP 72
38402 Saint Martin d'Heres Cedex
France
Subjet description
------------------
Formal methods have been shown to be applicable to the development of
safety critical systems. They are applied upstream to validate specifications
and downstream to prove code correctness. The B-Method is a framework,
based in theory on (Boolean) predicate transformers, for specifying,
designing and coding software systems. This method has been used to
develop significant industrial applications (for instance, the automatic
driver of the Paris subway Météor Line).
Embedded systems require strong constraints in matter of security and
efficiency. For example, memory ressources are strongly limited in smart
cards applications. The BOM RNTL project is concerned with the translation
of the B formal language into smart card code with optimized memory.
More precisely, specific techniques and tools will be defined to translate
the B0 language - the programming language of the B-method - to smart card
code. The translation process must be validated in order to ensure target
code correction. Memory optimizing algorithms can be complex and their
validation can be difficult. So, we shall tackle this problem by developing
optimization shemes which will be validated using the B-Method.
The goal of this work is to design theoretically well-founded and
actually implementable tools in order to assist memory optimizations.
The work will involve the construction of memory management optimization
schemes and investigations about extensions to the B-Method allowing the
implementation of these schemes.
The work will be conducted within a LSR team with a deep competence in
the B Method and the support tools. It will be done in close collaboration
with the partners from industry which are involved in the BOM project:
ClearSY, which maintains and markets the AtelierB, and GemPlus, the smart
cards and intelligent objects world leader.
============================================================================
--
----------------------------------------------------------------------------
Dr. Didier Bert http://www-lsr.imag.fr/users/Didier.Bert/
CNRS, Laboratoire LSR-IMAG Tel: 04 76 82 72 16 +33 476 82 72 16
681, rue de la Passerelle Fax: 04 76 82 72 87 +33 476 82 72 87
BP 72
38402 Saint-Martin-d'Heres CEDEX, France
----------------------------------------------------------------------------
|
