[TYPES/announce] FéRIA-IRIT PhD position on certified real-time code generator

[Marc Pantel]

PhD proposal in FéRIA-IRIT, Toulouse, France

Formal certification of code generator for hybrid systems

This proposal takes place in the GENE-AUTO project from the French
«Aerospace Valley» pole of competence in Toulouse. One of the key
approaches used is to leverage formal technologies to the level of
tackling real industrial problems.

The GENE-AUTO project aims at defining and implementing a certified
code generator for real-time critical embedded applications in
Automotive and Aerospace industries. This generator should take as
input high level hybrid models such as defined using
SimuLink/StateFlow (MathWorks TM) or SciCos and producing either human
readable C code or highly optimised assembly language for dedicated
architectures.

Currently, industrial code generator are only validated using
test-based framework. Many research work have been developed in order
to apply formal methods to this specific problem. Very good results
for domain specific languages, academic languages or subsets of
industrial languages have been obtained. However, bridging the gap
with a real-size industrial hybrid modelling language remains
a challenging task.

The purpose of the proposed PhD is to design a multi-pass approach in
order to tackle realistic optimising code generator with very strict
certification rules. A lot of intermediate languages will be used so
that the semantic bridge between each languages should be relatively
narrow. Each bridge can then be passed using the most appropriate
validation technology.

This work will be funded by GENE-AUTO industrial partners
(SIEMENS/VDO, AIRBUS, EADS-ASTRIUM, ALCATEL-ALENIA, BARCO, IAI)
through the IERSET.

This work will take place in the LYRE and ACADIE teams of IRIT
(Research Institute in Computer Science at Toulouse,
http://www.irit.fr), one of the biggest laboratory in Computer Science
in France located in Toulouse, one of the main design site for
Aerospace and embedded systems in Europe.

To have more information, please contact Marc.Pantel_at_enseeiht.fr
(replace _at_ with @).

Candidates should have a master degree in Computer Science, have
experiences using formal methods and be knowledgeable in language
engineering.