Le système de commande de vol (CDV) est un des systèmes les plus critiques à bord d'un avion. Les fonctions logicielles de ce système sont donc soumises à un effort de vérification important. Chez Airbus, le développement des fonctions critiques suit une approche basée sur des modèles formels, à partir desquels la majeure partie du code embarqué est générée. Certaines vérifications peuvent ainsi s'effectuer dès le niveau de la modélisation formelle, et sont aujourd'hui réalisées par test des modèles dans un environnement de simulation. L'objet de cette thèse est d'étudier comment une technique formelle, le model-checking, s'insère dans ces vérifications amonts. La contribution comporte trois parties. La première partie tire le bilan des études passées d'Airbus sur l'application du Model Checking au système de CDV. Nous analysons notamment les caractéristiques des fonctions de CDV, et leur impact sur l'applicabilité de la technologie. Le deuxième partie complète la précédente par une nouvelle étude, expérimentant le Model Checking sur la fonction Ground Spoiler de l'A380. Les expérimentations ont permis de consolider notre analyse du positionnement du Model Checking dans le processus Airbus. Un des problèmes pratiques identifiés concerne l'exploitation des contre-exemples retournés par le model-checker, en phase de mise au point d'un modèle. La troisième partie propose une solution à ce problème, basée sur l'analyse structurelle des parties d'un modèle activées par le contre-exemple. Il s'agit, d'une part d'extraire l'information pertinente pour expliquer la violation de la propriété cible et, d'autre part de guider le model-checker vers l'exploration de comportements différents, activant d'autres parties du modèle. Un algorithme d'analyse structurelle est défini, et implémenté dans un prototype afin d'en démontrer le concept.

Ce travail porte sur la programmation de systèmes de Contrôle-Commande. Ces systèmes sont constitués d'une boucle de contrôle qui acquiert l'état actuel du système par des capteurs, exécute des algorithmes de contrôle à partir de ces données et calcule les commandes à appliquer sur les actionneurs du système dans le but de réguler son état et d'accomplir une mission donnée. Ces systèmes sont critiques, leur implantation doit donc être déterministe, sur le plan fonctionnel (produire les bonnes sorties en réponse aux entrées) mais aussi sur le plan temporel (produire les données aux bonnes dates). Nous définissons un langage de description d'architecture logicielle temps réel et son compilateur pour programmer de tels systèmes. Il permet d'assembler les composants fonctionnels d'un système multirythme avec une sémantique formelle synchrone. Un programme consiste en un ensemble d'opérations importées, reliées par des dépendances de données. Des contraintes de périodicité ou d'échéance peuvent être spécifiées sur les opérations et un ensemble réduit d'opérateurs de transition de rythme permet de décrire de manière précise et non ambiguë des schémas de communication entre opérations de périodes différentes. Des analyses statiques assurent que la sémantique d'un programme est bien définie. Un programme correct est ensuite compilé en un ensemble de tâches temps réel concurrentes implantées sous forme de threads C communicants. Le code généré préserve la sémantique du programme original et s'exécute à l'aide d'un Système d'Exploitation Temps Réel standard disposant de la politique d'ordonnancement EDF.

L'optimisation multi-disciplinaire propose des solutions aux problèmes de conception de systèmes complexes. Le terme « optimisation multi-disciplinaire » laisse sous-entendre à tort qu'il ne s'agit que d'un problème d'optimisation. Nous lui préférons ici le terme de « conception collaborative ». En effet, l'optimisation ne représente qu'un aspect, qui ne peut être séparée du reste du problème de conception. Le but n'est pas de créer un processus automatique, mais de faciliter les échanges entre les équipes des différentes disciplines. De nombreuses méthodes, appelées communément formulations MDO (de Multi-Disciplinary Optimization), apparaissent dans la littérature (MDF, IDF, AAO, BLISS, CO). Elles proposent des stratégies permettant, d'une part, d'assurer la cohérence de la description du système complexe et, d'autre part, d'effectuer la recherche de la configuration optimale. Dans un premier temps, nous dressons un état de l'art des formulations MDO. Nous mettons en avant leurs points communs et leurs différences, afin de proposer une implémentation de la manière la plus générale qui soit. Nous proposons, avec la méthode DIVE (Discipline Interaction Variable Elimination), un cadre d'utilisation de méta-modèles au sein des formulations MDO. Le méta-modèle peut se limiter à une approximation linéaire ou quadratique. Il peut s'appuyer sur des méthodes classiques d'apprentissage, telles que les réseaux neuronaux, le Krigeage ou la SVM. Chaque méta-modèle est accompagné d'une région de confiance qui en détermine la validité. Cette approche par approximations locales et successives permet d'aborder les problèmes de grande dimension. Nous présentons des résultats obtenus avec deux cas-tests d'avions d'affaires supersoniques obtenus sous deux environnements différents (Scilab et ModelCenter).

La performance de la requête d’intersection, nécessaire à la simulation intensive de la propagation d’ondes, et indispensable aux rendus interactifs à base de lancer de rayons, est située au coeur du travail de cette thèse. En partant des meilleures structures de recherches et algorithmes de calculs d’intersections rayon/surface présents dans l’état de l’art, ce travail s’est concentré sur l’efficacité des groupes de rayons, sources de performance supplémentaire. Cependant, à l’inverse des rayons simples, la cohérence nécessaire aux groupes de rayons pose la problématique de leur organisation spatiale pour approcher la performance optimale. Après avoir montré comment construire et traiter efficacement les groupes de rayons avec deux structures de recherche particulières, le cas des rayons à origine commune a été étudié, et optimisé, pour l’évaluation des sources ponctuelles et de l’occlusion ambiante. Pour répondre à la problématique des rendus générant aussi bien des rayons cohérents que des rayons incohérents, une solution de couplage des structures de recherche est proposée en s’appuyant sur une stratégie globale d’affectation des rayons. Une autre solution, plus générale et destinée à exploiter la cohérence dans les cas les plus difficiles, est proposée pour regrouper automatiquement les rayons selon un critère a priori de cohérence. En se plaçant dans le contexte des modèles ayant une très forte complexité géométrique, la mise en place d’une pile de rayons, ainsi que sa distribution sur une grappe de calculateurs sont proposées afin d’améliorer la localité d’accès aux données, et de fournir une solution de visualisation interactive. Pour permettre la réorganisation automatique des rayons, et donc faciliter l’exploitation des groupes de rayons, cette thèse conclut qu’il est impératif de définir une nouvelle interface de programmation, en remplacement de la simple requête d’intersection.

Les travaux présentés dans ce manuscrit proposent une approche formelle pour la validation d'applications interactives Java-Swing vis-à-vis d'une spécification décrite par un modèle de tâches CTT. L'objectif de cette approche est de valider une partie de l'utilisabilité du système en s'appuyant sur l'extraction d'un modèle formel décrivant le comportement dynamique de l'application (modèle de dialogue). Cette extraction est obtenue par analyse statique du code source Java-Swing de l'application. La validation du système consiste alors à démontrer formellement que les structures d'interaction encodées dans le programme s'inscrivent bien dans les scénarii d'usage représentés en compréhension par le modèle de tâches CTT. Cette étape de validation exploite d'une part le modèle formel extrait par analyse statique et d'autre part une formalisation du modèle de tâches. La démarche d'extraction et de validation est abordée suivant deux techniques formelles distinctes : la méthode B événementielle basée sur la démonstration de théorèmes (theorem-proving), et la méthode NuSMV basée sur la vérification exhaustive de modèles (model-checking). Une étude de cas permet d'illustrer tout au long du mémoire la démarche de validation proposée suivant ces deux techniques formelles.

Le problème de l'exploitation commune de ressources limitées et coûteuses se pose très souvent dans le milieu industriel, et plus particulièrement dans le domaine spatial pour lequel les projets sont très souvent financés par plusieurs entités, pays ou organismes. L'exploitation de ces ressources doit bien entendu répondre à des critères d'efficacité, afin d'empêcher sa sous-exploitation, mais aussi à des critères d'équité, chaque agent espérant un retour sur investissement en rapport avec sa contribution financière. Nous nous sommes intéressés, au cours de ce travail de thèse, au problème de partage équitable de biens indivisibles (autrement dit d'objets) entre des agents, dont nous abordons trois aspects principaux : modélisation du problème, complexité et algorithmique. La modélisation du problème de partage que nous proposons s'inspire tout d'abord de la théorie du bien-être social et des nombreux travaux sur l'agrégation de préférences dans les problèmes de décision collective et de partage que l'on peut trouver dans le domaine du choix social et de la microéconomie. Elle s'appuie de plus sur un langage de représentation compacte inspiré des travaux sur l'expression logique de préférences. Nous nous intéressons dans un deuxième temps à la complexité du problème de partage tel qu'il a été défini, dont nous étudions deux aspects particuliers : complexité du problème de maximisation de l'utilité collective, et complexité du problème d'existence d'un partage efficace et sans envie. Enfin, dans la dernière partie du travail de thèse, nous nous penchons sur le problème de calcul d'un partage égalitariste au sens du leximin, problème pour lequel nous proposons et analysons plusieurs algorithmes fondés sur la programmation par contraintes. Ce travail de thèse s'appuie sur un problème réel d'allocation de prises de vue pour une constellation de satellites d'observation de la Terre.