Nous nous intéressons au développement prouvé de composants formels pour un générateur de code pré-qualifié. Ce dernier produit un code séquentiel (C et Ada) pour des modèles d'entrée qui combinent les flots de données et de contrôle et qui présentent des possibilités d'exécution concurrente (Simulink/Stateflow et Scicos). Le développement prouvé permet de réduire le coût des tests et d'augmenter l'assurance des outils développés avec cette approche vis-à-vis de la qualification. Les phases de spécification, de développement et de vérification des outils développés sont effectuées avec l'assistant de preuve Coq. Ce dernier permet d'extraire le contenu calculatoire des composants en préservant les propriétés prouvées en Coq. Ce code extrait est ensuite intégré dans une chaîne complète de développement (chaîne de GeneAuto). Nous présentons un cadre formel, inspiré de l'analyse statique, qui s'appuie sur la sémantique abstraite et qui est instanciable sur plusieurs composants du générateur de code. Nous nous basons sur les ensembles partiellement ordonnés et sur le calcul de point fixe pour définir le cadre et effectuer les différentes analyses des composants du générateur de code. Ce cadre formel comporte toutes les preuves communes aux composants et indépendantes des analyses effectuées. Deux composants sont étudiés : l'ordonnanceur et le typeur des modèles d'entrée. / We are interested in the proved development of formal components for a pre-qualified code generator. This produces a sequential code (C and Ada) for input models that combine data and control flows, with potential concurrent execution (Simulink/Stateflow and Scicos). The proved development reduces test cost and increases insurance of components developed with this approach regarding the qualification. Phases of specification, development and verification of the developed components are done with the Coq proof assistant. This allows to extract the computational content of the components preserving the properties proved in Coq. The extracted code is then integrated into the complete development tool-chain (GeneAuto tool-chain). We present a formal framework, inspired from static analysis, based on the abstract semantics which is instantiable to several components of the code generator. We rely on partially ordered sets and fixed-point to define de formal framework and to perform the various analysis of components of the code generator. This formal framework includes all proofs common to the components and independent from the performed analyses. Two components are studied : the scheduler and the type checker of input models.

Notre étude s’intéresse à l’agence André entre 1929 et 1973, période d’activité des frères Jacques et Michel André, architecte et ingénieur. Nous interrogeons leur production dans son contexte spatial et historique, à la lumière des notions de filiations et de réseaux. Issus d’une importante dynastie d’architectes en Lorraine, ils bénéficient d’un héritage à la fois matériel et intellectuel. Cet ancrage, soutenu par la foisonnante École de Nancy du début du siècle, favorise les réseaux de proximité comme les échanges culturels internationaux. Les frères André prolongent ce dynamisme critique en s’impliquant dans le Comité Nancy-Paris,l’Union des artistes modernes et la revue L’Architecture d’aujourd’hui. Dans l’Entre-deux guerres,ils sont les premiers architectes à collaborer durablement avec Jean Prouvé, avant d’associer à l’agence Claude, le fils de ce dernier, dans les années 1960. Proche des entrepreneurs locaux, les deux frères questionnent la valeur constructive de l’architecture :ils s’attachent à atteindre la perfection technique et expérimentent les matériaux. Cette recherche traverse leur production, depuis leur première grande réalisation, l’Institut de zoologie, inspiré par les procédés de Frank Lloyd Wright, jusqu’au musée de l’Histoire du fer,symbole de gloire industrielle régionale. Tandis que les années 1930 constituent une période d’intense créativité, l’agence développe après-guerre les outils nécessaires pour faire face à une commande massive, notamment postale, et se met en quête de productivité. L’agence des frères André constitue ainsi un témoin privilégié des bouleversements de la production architecturale au cours du XXème siècle. / Our study focuses on the André agency between 1929 and 1973, period of activity of thebrothers Jacques and Michel André, architect and engineer. We question their production inits spatial and historical context, in the light of the notions of filiation and networks. Comingfrom a large dynasty of architects in Lorraine, they benefit from both material and intellectuallegacy. This rooting, supported by the teeming École de Nancy in the early century,promotes close networks as well as international cultural exchanges. The André brothersextend this critical dynamic by getting involved in the Comité Nancy-Paris, the Union desartistes modernes (UAM) and the L'Architecture d'aujourd'hui magazine. During the Interwarperiod, they were the first architects to work sustainably with Jean Prouvé, before associatingClaude, the son of the later, to the agency in the 1960s. Close to local building contractors,the two brothers question the constructive value of architecture: they focus on reaching ontechnical perfection and experimentation on materials. This research goes through theirproduction, since their first major achievement, the Institute of Zoology, inspired by FrankLloyd Wright’s processes, to the museum of iron history, symbol of the region's industrialglory. While the 1930s are a period of creativity, the agency develops postwar the toolsneeded to face intense order, in particular postal, and shifts toward a quest for productivity.The André agency thus constitutes a privileged witness to the upheavals of architecturalproduction during the 20th century.