Les travaux développés dans ce mémoire se situent à l'intersection des domaines du Génie Logiciel et de l'Intelligence Artificielle Distribuée : l'objectif est de spécifier un système d‘aide à la gestion d'information au sein d'une organisation de type administrative complexe sous la forme d'un système multi-agent. Le modèle holonique a été choisi, suite à une étude générale sur les organisations humaines et sur les organisations multi-agent, afin de structurer un système d'aide distribué en adéquation avec notre problématique, à savoir l'apport d'une aide au niveau de chaque acteur de l'organisation et la gestion de la cohérence de son fonctionnement global. Le choix d'une méthode d'analyse et de modélisation de système administratif complexe a nécessité la confrontation, à l'aide d'un benchmark, d'un ensemble de méthodes issues du Génie Logiciel et couramment utilisées. Aucune des méthodes comparées ne répondant totalement aux critères établis, la méthode MAMOSACO, conçue par adaptation et intégration des éléments les plus pertinents des méthodes comparées, est proposée. Cette méthode permet de spécifier un Système Orienté Holon pour l'aide au Travail COopératif (SOHTCO) d'un ensemble des acteurs impliqués dans une procédure donnée. La méthode MAMOSACO a été appliquée, au travers de son atelier de modélisation, sur un ensemble de cas réels de procédures administratives complexes. Et, finalement, sur base du cas d'application développé, un ensemble de perspectives de recherches, tant en ce qui concerne la modélisation qu'en ce qui concerne le système multi-agent holonique, est proposé.

Nous présentons un ensemble de travaux sur l'intégration de méthodes formelles et l'analyse multifacette de systèmes logiciels. %deuxième partie Partant de l'idée que les différentes facettes d'un système doivent être étudiées et développées avec les formalismes et outils appropriés, nous avons exploré, suite à d'autres chercheurs, des pistes pour l'intégration de méthodes formelles utilisées pour spécifier, analyser ou développer des parties des systèmes. La nécessité de l'intégration est relative au besoin de l'interaction entre différentes parties d'un même système ou bien à l'appréhension globale des propriétés du système. Nous explicitons les principaux problèmes de l'intégration de méthodes formelles : l'hétérogénéité syntaxique, l'hétérogénétité sémantique et la variété des systèmes logiques de raisonnement. Nous proposons alors la notion de compatibilité relative à ces trois niveaux pour assurer l'intégration de méthodes. L'idée principale est celle de l'interopérabilité sur une base sémantique (base d'intégration) ) sans laquelle aucun raisonnement n'est possible entre des parties assemblées d'un système. Les raisonnements formels sont alors effectués par plongement (embedding) des spécifications dans des logiques appropriées. Ce premier cadre est généralisé à des domaines de compatibilité plus larges que les bases d'intégration, et qui permettent de s'affranchir des langages et de travailler au niveau des paradigmes sous-jacents aux langages ; on obtient ainsi un cadre pour une intégration générique. Nous avons montré comment les formalismes intégrés existants tels que LOTOS, CSP-B, Circus rentrent dans ce cadre et nous avons mis en oeuvre ces idées pour de nouvelles intégrations par exemple B et les réseaux de Pétri. Dans une autre partie des travaux, nous présentons des extensions proposées autour de la méthode B, notamment la composition parallèle asynchrone de systèmes abstraits B à la manière de la composition parallèle dans les algèbres de processus. Notre proposition permet de combiner dans un même projet de développement formel la démarche descendante de la méthode B par une approche ascendante. Nous présentons ensuite une méthode de construction systématique de spécifications B pour des systèmes multi-processus à architecture dynamique. Ces travaux généralisent les précédents sur la composition de systèmes abstraits en définissant un opérateur de fusion de sous-systèmes qui est plus général que les opérateurs de composition parallèle. Une partie des travaux est consacrée à l'analyse multifacette de système ; notre proposition consiste à assurer la compatibilité des analyses des différentes facettes en partant non pas de modèles indépendants mais de modèles spécifiques dérivés à partir d'un modèle de référence qui permet d'assurer la cohésion globale de l'analyse. Cette approche est poursuivie par des expérimentations sur la combinaison de prouveurs et d'évaluateurs de modèles (model-checkers). Nous avons exploré d'autres voies pour l'analyse multifacette : élaborer une algèbre de spécifications multiparadigmes, ou différents aspects, relatifs aux facettes envisagées, peuvent être introduits dans une même unité de spécification. Les unités de spécification sont ensuite composées à l'aide des opérateurs de l'algèbre. Le lien est fait entre cette approche et celle de l'intégration de méthodes par plongement dans des logiques formelles. Une plateforme expérimentale est développée conjointement à ces travaux et relie les deux approches : elle permettra à terme de traduire, moyennant la compatibilité sémantique, différents formalismes d'entrées dans des formalismes cibles en passant par un modèle de référence ou pivot qui lui même est une spécification multiparadigme.

Les exigences qui s'appliquent aux composants logiciels et aux logiciels embarqués justifient l'utilisation des meilleures techniques disponibles pour garantir la qualité des spécifications et conserver cette qualité lors du développement du code. Les méthodes formelles, et parmi elles la méthode B, permettent d'atteindre ce niveau de qualité. Cependant, ces méthodes utilisent des notations et des concepts spécifiques, qui génèrent souvent une faible lisibilité et une difficulté d'intégration dans les processus de développement et de certification. Ainsi, proposer des environnements de spécification, de développement de programmes et de logiciels, combinant des méthodes formelles et des méthodes semi-formelles largement utilisées dans les projets industriels, en l'occurrence B et UML, s'avère d'une grande importance. Notre intérêt porte précisément sur la méthode B qui est une méthode formelle utilisée pour modéliser des systèmes et prouver l'exactitude de leur conception par raffinements successifs. Mais les spécifications formelles sont difficiles à lire quand elles ne sont pas accompagnées d'une documentation. Cette lisibilité est essentielle pour une bonne compréhension de la spécification, notamment dans des phases de validation ou de certification. Aujourd'hui, en B, cette documentation est fournie sous forme de texte, avec, quelquefois, des schémas explicitant certaines caractéristiques du système. L'objectif de ce travail de thèse est de mettre en relation des spécifications en B avec des diagrammes UML, qui constituent un standard de facto dans le monde industriel et dont le caractère graphique améliore la lisibilité. Nous avons axé notre processus de dérivation de diagrammes de classes à partir de spécifications B autour d'une technique d'ingénierie inverse guidée par un ensemble de correspondances structurelles et sémantiques spécifiées à un méta-niveau. Quant à la dérivation de diagrammes d'états/transitions, elle a été orientée vers une technique d'abstraction de graphes d'accessibilité construits par une exploration exhaustive du comportement de la spécification.