A ce jour, les méthodes formelles ont montré qu'elles étaient applicables avec succès au développement de logiciels industriels. Pour maîtriser la complexité croissante de ces applications, la mise en oeuvre des paradigmes d'abstraction et de composition est incontournable. La méthode B permet d'assister le processus de développement des spécifications au code et offre une notion de modularité qui permet de composer à la fois les spécifications et les développements. La compositionnalité des preuves est assurée par des restrictions imposées par le langage, qui limitent les formes d'architectures autorisées. A la suite de nos précédents travaux, le manuscrit présenté ici explicite les principes de composition des spécifications et des développements, énonce les théorèmes sous-jacents à la composition des preuves et complète et valide les restrictions imposées par la méthode B. Bien que dédiés à la méthode B, les résultats présentés sont plus généraux : ils peuvent s'appliquer à d'autres approches formelles basées sur la notion d'état, comme les approches objet

Je présente dans ce mémoire un bilan de mon activité scientifique effectuée au sein des groupes POC (Parallèlisation et Optimisation Combinatoire) et SID (Systèmes d'Information Distribués) de l'équipe ROI (Recherche Opérationnelle et Informatique) du laboratoire LAMIH à l'UVHC. <br /><br />Mes travaux de recherche se divisent en trois parties:<br /><br /> - l'étude du problème du sac-à-dos non borné, problème classique de l'optimisation combinatoire, dont nous mettons en évidence des propriétés fondamentales et pour lequel nous avons dérivé, implanté et mis à disposition deux algorithmes qui tirent avantage des propriétés découvertes;<br /><br /> - une approche algorithmique parallèle/distribuée pour la<br /> bio-informatique notamment le problème de repliement de protéïnes qui est un problème reconnu comme l'un des plus difficiles posés à la science informatique dans le contexte de la bio-informatique;<br /><br /> - le développement d'une plate-forme ouverte d'expérimentations pour la méthode formelle B, l'étude de la modularité du langage B et d'extensions de B pour générer des composants logiciels ainsi que l'étude de l' adjonction au langage B d'une logique temporelle.<br /> <br /> Nous montrons comment les approches utilisées dans une recherche en optimisation combinatoire d'une part et en spécification formelle d'autre part peuvent s'enrichir et se féconder mutuellement.