This thesis aimed at providing a method to model, verify, and generate allocations of embedded systems functions on avionics resources. This method is based on the use of AltaRica language to formally describe the propagation of failures within an embedded system, on the use of verification techniques such as "model-checking" and use of problem-solving based on constraints. The work is illustrated by two case studies: allocation of an aircraft function "terrain-following" on computing and communication resources on an existing fighter, positioning of equipment of a hydraulic system in an aircraft taking into account risks such as a tire burst or an engine burst.
