Abstract interpretation of ACSL annotations
Frama-C is a set of tools dedicated
to the analysis of C software. In Frama-C, different analyses
techniques are implemented as plug-ins within the same framework.
Part of the glue that holds the various plug-ins together is
the ACSL annotation language. ACSL is a formal specification
language for C programs.
Each verification plug-in is supposed to interpret ACSL
annotations as best it can. A plug-in can also, when it needs to
make an assumption, express it as an ACSL property so that
another plug-in can be used to verify this assumption.
This post-doctoral position consists in improving the precision of Frama-C’s value analysis, based on Abstract Interpretation, for constructs that are not currently handled. The treatment of some constructs will require specific abstract domains to be designed.
http://frama-c.com
http://frama-c.com/value.html
http://frama-c.com/acsl.html
Multiscale Modeling of the Degradation Mechanisms in Polymer Electrolyte Fuel Cells
In an attempt to provide a rigorous physical-based description of the physicochemical phenomena occurring in the PEFC environments, the Modeling Group at CEA-Grenoble/LCPEM has developed a novel physical multi-scale theory of the PEFC electrodes electro-catalysis,the MEMEPhys model, based on a combined non-equilibrium thermodynamics/electrodynamics approach. This postdoctoral research position will consist on actively contributing on the development of the model, including the implementation of a physical-based description of water transport phenomena and water condensation in the PEFC. Heterogeneities on the electrochemical and aging processes, induced by water transport, will be in particular addressed. The candidate will strongly combine theoretical and experimental data, obtained in our laboratory, in order to establish MEA microstructure-performance relationships and to elucidate the main MEA degradation and failure mechanisms. From a fundamental point of view, this work will provide a deeper understanding of the electrochemical mechanisms responsible of the PEFC active layers aging at different spatiotemporal scales.
Study and realization of thermal energy harvesting prototypes by thermal/fluidic coupling, and then electrical conversion. Application to electronic circuits.
The objective of this study is to explore possibilities of using systems with fluidic/thermal coupling to harvest the thermal energy released by an electronic device and then convert it into electricity that can be stored or used again. In those systems, the fluidic can be also used for a cooling purpose.
The two main steps will be the design of devices allowing controlling the operating regimes of the fluidic system submitted to a constant heat source (thermo-fluidic coupling) and the characterization of the best coupling conditions with the electrical conversion devices, in particular piezo-electrical. The studies will also explore new mechanisms taking place in the small scale fluidic systems compared to models known macroscopically. The work will be mostly experimental but will also include a simulation part.
The study should also provide an estimation of the harvesting efficiency as well as the power densities taking place in this kind of new devices.
Process evaluation of 3rd generation biofuel production from micro-algae
CEA contributes to R&D activities in 3rd generation biofuel production from micro-algae by its fundamental research in biology (understanding of biological mechanism and improvement of microorganism performances) led by DSV at CEA Cadarache. LITEN Institute, belonging to CEA/DRT, investigates 2nd biofuel generation, from studies on resources (biomass, waste) up to industrial, economical and environmental integration.
This post doc fellow will use the different approaches developed at LITEN/DTBH to :
- perform a prospective study on process integration, for biofuel production from micro-algae,
- realize a technico-economical study of the more promising process solutions in the 2rd generation domain and industrial use of micro-algae,
- estimate the environmental impact (especially CO2) of these processes.
This work will take place in in frame of a collaboration of both labs (DSV/IBEB and DRT/LITEN/DTBH), the first one bringing its very fundamental knowledge on technical ability and performance of the micro-organism, the second one giving the knowledge on process and technico-economical evaluation of industrial reactor systems.
The post doc fellow, located in Grenoble, will go as needed in Cadarache to discuss with biology experts.
modelling and Control of voltage and frequancy in GALS architecture submitted to Process-Voltage-Temperature variability
The evolution of sub-micron technologies has induced tremendous challenges the designer has to face, namely, the Process-Voltage-Temperature varibility and the decrase of power consumption for mobile applications.
The work to be done here concerns the DVFS (Dynamic Voltage and Frequency Scaling) policies for GALS (Globally Asynchronous, Locally Synchronous) architecture.
A fine grain modelling of the voltage and frequency “actuators” must be first done in order to simulate in a realistic ways the physical phenomena. Especially, the various parameters that may influence the system will be considered (process variation, supply voltage variation and noise, temperature variation, etc.)
Then, Non-Linear (NL) control laws that take into account the saturation of the actuators will be developed. These laws will be validated on the physical simulator and their performances in regulation (i.e. the response of the closed-loop system to disturbances such as PVT variations) will be evaluated. Note that these laws will be designed at the light of implementation constraints (mainly cost) in terms of complexity, area, etc.
Actually, the system considered here is intrinsically a Multi-Inputs-Multi-Outputs (MIMO) one. Therefore, its control can be design with NL techniques devoted to MIMO systems in order to ensure the requirements and reject the disturbances.
The control of several Voltage and Frequency Islands (VFI) is usually done via a “central brain” that chooses the voltage and frequency references thanks to a computational workload deadline. For more advanced architectures, the capabilities of each processing element, especially its maximum frequency, can be taken into account. A disruptive approach should be to consider a more distributed control that for instance takes into account the particular state (e.g. temperature) of each VFI neighbours. Control techniques that have been designed for distributed Network Controlled Systems could be adapted to MPSoCs.
Integrated antenna arrays for 60 GHz high-data rate communications
This post-doctoral offer is in support of our work program on the design of millimetre-wave antennas for high data rate communication systems in the 57-66 GHz frequency band. The realization of smart devices in this frequency band with a high level of integration and a low cost is a challenge accessible today thanks to the recent microelectronic technologies as well as other silicon technologies such as assembly, packaging or micromachining. Some applications in the consumer electronics domain are clearly identified and expected to result in product in a very short term.
After a series of project completed these last years on the design of single antennas built and validated on different technologies, such as silicon or ceramic, the future projects will focus on the demonstration of antenna arrays with electronic beamsteering for long range applications. Several demonstrators will be realized in collaboration with our partners developing the integrated circuits and fabrication/assembly technologies in order to obtain a fully functional system.
Metamaterials : design of an integrated high-impedance surface at 60 GHz, transposition and potentialities at 60 THz
Invisibility cloaking, sub-wavelength, thin antenna substrates, absorbers, etc., metamaterial structures have open many perspectives, some of them seeming futuristic while other being very practical given the current ste of the art in the domains of materials, microtechnologies and integrated optics.
this post-doctoral work will focus on the study of high-impedance surfaces and the possibility of transposition of these designs between very different frequency bands (6 GHz, 60 GHz, 60 THz) corresponding to a wide range of technologies and applications.
After a thorough bibliographic study of the current state of the art, the developments will include the design of high-impedance surfaces at the three frequency bands cited above and an experimental demonstration at 6 GHz and possibly at 60 GHz.
Global offshore wind turbines monitoring using low cost devices and simplified deployment methods
This project follows previous work focused on on-shore wind turbine instrumentation with inertial sensors networks whose dataflows allows the detection of vibration modes specific to the wind turbine components, in particular the mast and the real-time monitoring of these signals.
The objectives of this project are manyfolds: to bring this work to offshore wind turbines; search for signatures in wider frequency bands; study the behavior of offshore platforms and their anchorages.
One of the challenges is to find the signatures of rotating elements (blades) without direct instrumentation. Instrumentation of these elements is indeed more expensive and more impacting on the structure.
In addition, the sensor technology will be suitable for monitoring the fatigue life cycle of moving wire structures (dynamic electrical connection cable and anchoring) in the case of an off-shore wind turbine. The ultimate goal is to propose a global method for offshore wind turbine health monitoring.
Sizing and control optimisation of a hydrogen production system coupled with an offshore wind farm
Coupling MRE (Marine Renewable Energy) and hydrogen sectors reveal an important potential long-term assets. The MHyWind project suggests to estimate the energetic and economic potential of a hydrogen production system integrated into a substation of an offshore wind farm. The hydrogen produced and stored locally will be distributed by boat for harbour uses, as a replacement of fossil fuels. For that purpose, it will be organized a simulation which will integrate all the energy chain towards the harbour uses of hydrogen. It will allow to estimate various configurations and sizing according to the local uses, valuation leverages, control modes and behavior of the system. The criteria will be the producible (kg of H2 producted and used) and complet costs (CAPEX and OPEX). The objective of the postdoctoral student will be to develop the simulation tool on this applicative being fully integrated with the teams of concerned laboratories.