Les spécifications formelles et la modélisation par objets sont considérés comme deux champs ayant un fort potentiel d'influence sur l'avenir du génie logiciel. Dans un premier temps, nous étudions cette affirmation en dégageant les caractéristiques essentielles du développement du logiciel. L'intersection des deux champs est un domaine nouveau et prometteur. Nous en étudions les différents variantes et nous synthétisons les choix faits dans les méthodes formelles à objets actuelles. Dans ce contexte, cette thèse propose une méthode de spécification et de conception de composants logiciels destinée à faciliter la formalisation, automatiser partiellement le processus de conception, permettre le contrôle et la réutilisation des classes avant implantation. L'accent est mis sur la séparation entre les niveaux de description pour clarifier le processus de conception et sur l'uniformisation à l'intérieur des niveaux de description pour assurer la cohérence. Deux modèles sont décrits. Le premier modèle, dit des types abstraits graphiques, définit les composants suivant un axe dynamique et suivant un axe fonctionnel. La modélisation dynamique, naturelle pour des objets est donnée en termes d'automates d'états finis gardés. Outre sa lisibilité, le modèle dynamique a pour intérêt majeur la construction guidée de spécifications algébriques, support de l'axe fonctionnel. Le second modèle, dit des classes formelles, est un modèle général, formel et abstrait pour la conception à objets. Basé sur les types abstraits algébriques, il permet le raisonnement abstrait et ma mise en oeuvre dans différents langages de programmation à objets. Les modèles présentés sont indépendants et sont adaptables dans d'autres méthodes de développement. Nous proposons une méthode de transition entre ces deux modèles, qui favorise le contrôle et la réutilisation des spécifications. Plusieurs outils d'écriture et de preuve sont communs aux deux modèles et nous insistons sur l'ouverture vers d'autres environnements de spécification.

Cette thèse traite des mesures des flux d'information dans les systèmes informatiques. Nous exploitons les similarités entre des différents scénarios où la sécurité est une préoccupation, et nous appliquons les concepts de la théorie de l'information pour évaluer le niveau de protection offerte. Dans le premier scénario, nous considérons le problème de la définition des fuites d'information dans les systèmes interactifs où les éléments secrets et les éléments observables peuvent s'alterner au cours du calcul. Nous montrons que l'approche classique de la théorie de l'information qui interprète des systèmes tels que des canaux bruités (simples) n'est plus valide. Toutefois, le principe peut être récupéré si l'on considère les canaux d'un type plus compliqué, que, dans Théorie de l'information sont connus en tant que canaux avec mémoire et rétroaction. Nous montrons qu'il existe une correspondance parfaite entre les systèmes interactifs et ce type de canaux. Dans le deuxième scénario, nous considérons le problème de la vie privée dans les bases de données statistiques. Dans la communauté des bases de données, le concept de Differential Privacy est une notion qui est devenue très populaire. En gros, l'idée est qu'un mécanisme d'interrogation aléatoire assure la protection suffisante si le rapport entre les probabilités que deux ensembles de données adjacentes donnent la même réponse est lié par une constante. On observe la similarité de cet objectif avec la principale préoccupation dans le domaine des flux de l'information: limiter la possibilité de déduire les éléments secrets à partir des éléments observables. Nous montrons comment modéliser le système d'interrogation en termes d'un canal d'information-théorique, et l'on compare la notion de Differential Privacy avec le concept information mutuelle basé sur le travail de Smith. Nous montrons que Differential Privacy implique une borne sur l'information mutuelle, mais pas vice-versa. Nous avons également réfléchir à l'utilité du mécanisme de randomisation, ce qui représente la proximité entre les réponses aléatoires et les vraies, en moyenne. Nous montrons que la notion de Differential Privacy implique une borne serrée sur l'utilité, et nous proposons une méthode qui, sous certaines conditions, construit un mécanisme de randomisation optimale. Déménagent de l'accent mis sur des approches quantitatives, nous abordons le problème de l'utilisation des équivalences des processus pour caractériser des propriétés de protection d'information. Dans la littérature, certains travaux ont utilisé cette approche, fondée sur le principe selon lequel un protocole P avec une variable x satisfait de ces biens si et seulement si, pour chaque paire de secrets s1 et s2, P [s1 / x] est équivalent à P [s2 / x]. Nous montrons que, en présence de non-déterminisme, le principe ci-dessus repose sur l'hypothèse que le scheduler "travaille pour le bénéfice du protocole", et ce n'est généralement pas une hypothèse valable. Parmi des équivalences non-secoures, en ce sens, il y a l'équivalence des traces complètes et la bisimulation. Nous présentons un formalisme dans lequel on peut spécifier schedulers valides et, en conséquence, des versions sécurité des équivalences sur dessus. Nous montrons que notre version de bisimulation est toujours une congruence. Enfin, nous montrons que nos équivalences de sécurité peuvent être utilisées pour établir les propriétés de protection d'information.

L'architecture logicielle est devenue un thème scientifique majeur de l'informatique. En effet, l'architecture logicielle fournit l'abstraction qui permet de développer rigoureusement et de faire évoluer des systèmes logiciels complexes au vu des besoins tant fonctionnels que non fonctionnels. Afin de modéliser les architectures logicielles, un nouveau type de langage est apparu : les langages de description d'architectures (ADL, Architecture Description Language). Divers ADL ont été proposés dans la littérature, mais ces ADL sont restreints à la modélisation d'architectures abstraites, indépendantes des plateformes d'implémentation. Lors de l'implémentation, l'architecture n'est plus représentée. Cette thèse s'inscrit dans le domaine des ADL et porte sur la définition et la mise en œuvre d'un langage pour la concrétisation, c'est-à-dire l'implémentation explicite, d'architectures logicielles. Elle adresse le problème de la construction d'un tel langage et son système d'exécution. Pour cela elle aborde le problème d'un point de vue nouveau : la construction d'un langage centré sur l'architecture logicielle. Assis sur des bases formelles, notamment sur le π-calcul et π-ADL, ces travaux ont donné lieu à un langage formel pour décrire et garantir l'intégrité architecturale d'un système au niveau de sa spécification, de son implémentation et de ses évolutions ultérieures. La machine virtuelle et le compilateur associé sont enfouis dans la plateforme .NET.

Les phases de validation et de vérification (V&V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS.

Cette thèse traite de l'intégration de bases de données topographiques qui consiste à expliciter les relations de correspondance entre bases de données hétérogènes, de sorte à permettre leur utilisation conjointe. L'automatisation de ce processus d'intégration suppose celle de la détection des divers types d'hétérogénéité pouvant intervenir entre les bases de données topographiques à intégrer. Ceci suppose de disposer, pour chacune des bases à intégrer, de connaissances sur leurs contenus respectifs. Ainsi, l'objectif de cette thèse réside dans la formalisation, l'acquisition et l'exploitation des connaissances nécessaires pour la mise en œuvre d'un processus d'intégration virtuelle de bases de données géographiques vectorielles. Une première étape du processus d'intégration de bases de données topographiques consiste à apparier leurs schémas conceptuels. Pour ce faire, nous proposons de nous appuyer sur une source de connaissances particulière : les spécifications des bases de données topographiques. Celles-ci sont tout d'abord mises à profit pour la création d'une ontologie du domaine de la topographie. Cette ontologie est utilisée comme ontologie de support, dans le cadre d'une première approche d'appariement de schémas de bases de données topographiques, fondée sur des techniques d'appariement terminologiques et structurelles. Une seconde approche, inspirée des techniques d'appariement fondées sur la sémantique, met en œuvre cette ontologie pour la représentation des connaissances sur les règles de sélection et de représentation géométrique des entités géographiques issues des spécifications dans le langage OWL 2, et leur exploitation par un système de raisonnement

Les travaux décrits dans ce manuscrit de thèse s'inscrivent dans le cadre des méthodes formelles pour les langages de spécifications formées d'automates communicants. Ce type de langage est largement utilisé dans les industries de pointe où le niveau de fiabilité requis est élevé (e.g. aéronautique, transports), car ils permettent d'améliorer la précision des spécifications et d'exploiter des outils de simulation, de test ou de vérification qui contribuent à la validation des spécifications. Un frein au passage à l'échelle industrielle de ces méthodes formelles est connu sous le nom de l'explosion combinatoire, qui est due à la fois à la manipulation de larges domaines numériques, et au parallélisme intrinsèque aux spécifications.<br />L'idée que nous proposons consiste à contourner ce phénomène en appliquant des techniques de réduction paramétrée, pouvant être désignées sous le terme anglo-saxon "slicing'', en amont d'une analyse complexe. Cette analyse peut ainsi être effectuée a posteriori sur une spécification réduite, donc potentiellement moins sujette à l'explosion combinatoire. Notre méthode de réduction paramétrée est basée sur des relations de dépendances dans la spécification sous analyse, et est fondée principalement sur les travaux effectués par les communautés de la compilation et du slicing de programmes. Dans cette thèse nous établissons un cadre théorique pour les analyses statiques de spécifications formées d'automates communicants, dans lequel nous définissons formellement les relations de dépendances mentionnées ci-dessus, ainsi que le concept de "tranche" de spécification par rapport à un "critère" de réduction. Ensuite, nous décrivons et démontrons les algorithmes efficaces que nous avons mis au point pour calculer les relations de dépendances et les tranches de spécifications, et enfin nous décrivons notre mise en oeuvre de ces algorithmes dans l'outil "Carver", pour la réduction paramétrée de spécifications formées d'automates communicants.

Le travail coopératif est un domaine qui étudie le travail de groupes d'utilisateurs de façon générale. Sa finalité est la conception de collecticiels, ensembles logiciels qui contiennent les outils, les applications, et les plate-formes qui supportent les activités de groupes d'utilisateurs. La gestion de ces groupes et les échanges d'information entre leurs membres nécessitent la définition de nouveaux services de communication adaptés aux besoins des agents en coopération. Les travaux menés dans ce mémoire ont consisté à définir, à concevoir et à gérer la structuration des groupes coopératifs. Un modèle à base de graphes a été proposé à partir du partage de données, pour représenter les relations entre les divers membres d'un groupe coopératif. A partir de ce modèle, un service pour l'entrée et la sortie en coopération des agents coopérants a été défini. Un protocole de communication sous-jacent a été spécifié en utilisant le langage de description formelle Estelle. Le protocole proposé a été vérifié en utilisant l'environnement à base de réseaux de Petri VAL, puis a été implanté en langage C sous UNIX à partir du code Estelle généré. Une extension de ce travail permet la formation d'apartés qui sont des sous-groupes très dynamiques créés à l'intérieur de la coopération. Un autre protocole spécifié en Estelle a été proposé pour gérer la formation de ces apartés et leur évolution au sein de la coopération. En plus de la structuration des groupes, une étude des données qui peuvent être échangées entre des agents coopérants a mené à la définition d'un service de gestion des dépendances de données. Ce service, spécifié également en Estelle, permet de créer, supprimer ou modifier des dépendances entre données, et répercute les modifications de valeurs vers l'ensemble des données dépendantes.

Cette thèse s'inscrit dans le cadre de la conception des systèmes mécatroniques et porte, plus particulièrement, sur le dimensionnement de chaînes d'actionnement et les méthodes à mettre en œuvre pour satisfaire le cahier des charges et réduire au mieux le temps de développement. Afin de suivre l'évolution du marché et faire face à la concurrence croissante, les concepteurs ont eu recours au cycle de conception en Vet au prototypage virtuel. Pour réduire davantage la durée du processus de conception, la formulation du problème de conception sous la forme d'un problème inverse est une solution intéressante. Dans ce contexte, le laboratoire Ampère propose une méthodologie de dimensionnement par modèles bond graph inverses. Ainsi, l’objectif de cette thèse est de contribuer au développement de cette méthodologie d'une part dans sa phase de vérification de l'adéquation des spécifications du cahier des charges à la structure retenue pour le modèle de conception et, d'autre part, par la prise en compte des tolérances dans le problème de conception. Pour la phase de vérification de l'adéquation spécifications/structure, le mémoire présente tout d'abord, l’analyse structurelle du cahier des charges qui permet de vérifier, avant toute simulation et à partir du modèle bond graph, si le problème de conception par modèle inverse est bien posé. Différents niveaux d’analyse sont supposés pour renforcer la démarche chronologique du travail de conception ou de reconception proposée par la méthodologie de dimensionnement. Ensuite, ces niveaux d'analyse sont mis à profit pour définir une procédure de vérification de l'adéquation des spécifications, définies sous forme de comportements type, au modèle de conception. En cas d'inadéquation, des recommandations pour la remise en question des spécifications ou de la structure du modèle de conception sont proposées et ce, selon le niveau d'analyse considéré. Au niveau de l'analyse numérique (le niveau d'analyse le plus bas), cette procédure peut être utilisée pour la synthèse paramétrique ou encore pour la synthèse de tolérance en cas de prise en compte des incertitudes dans le problème de conception. Concernant cet aspect, le mémoire présente également une contribution à la représentation des incertitudes paramétriques dans le formalisme bond graph, formalisme de base de la méthodologie de dimensionnement. Enfin, l'approche probabiliste est utilisée pour la modélisation des incertitudes dans la démarche de dimensionnement des systèmes dynamiques par inversion des modèles bond graph : les deux cas d'inversion, entrées/sorties d'une part (pour la remontée de spécifications), et paramètres/sorties d'autre part (pour la synthèse de tolérances paramétriques), sont abordés. Les règles d'exploitation d'un modèle bond graph probabiliste permettant la propagation des fonctions de densité de probabilité et des grandeurs caractéristiques(espérance et variance) tout le long de la structure énergétique du système sont proposées et illustrées par un exemple. / No abstract

La montée en puissance des enjeux environnementaux incite les industriels de la mécanique à intégrer la dimension environnementale dans le processus de conception de leurs produits. Un nouveau contexte de conception émerge : les fournisseurs sont de plus en plus fortement impliqués dans les processus de leurs clients. Ils atteignent, de ce fait, un niveau de responsabilité élevé et peuvent, par leurs actions, fortement influencer la performance environnementale d’un système final. Il devient ainsi nécessaire de favoriser l’intégration de la dimension environnementale au sein des relations entre clients et fournisseurs. Cette intégration se confronte à trois verrous majeurs : (1) un verrou organisationnel qui est lié le déficit d’intégration de l’environnement au sein des différents niveaux hiérarchiques d’une organisation, (2) un verrou opérationnel qui concerne le manque d’expertise environnemental, limitant la pérennité de l’intégration la dimension environnementale dans le processus de conception des entreprises, (3) un verrou relationnel qui est lié à une relation déséquilibrée entre clients et fournisseurs. Nos travaux aboutissent au développement de la méthode GECO (Gestion de L’Environnement dans la relation Client/fOurnisseur). Elle se destine à l’accompagnement des entreprises de la mécanique dans une gestion cohérente, pro-active et sur-mesure de la dimension environnementale avec leurs clients et fournisseurs. D’abord, elle permet d’établir le diagnostic des enjeux environnementaux clients devant être pris en compte à court et à long terme. Le but est de faire apparaître les enjeux nécessitant une montée en compétence rapide afin d’anticiper les futures évolutions sectorielles. La méthode propose, dans un seconde temps, un ensemble d’actions et d’outils d’éco-conception à mette en place afin d’accompagner cette montée en compétence. Enfin, la méthode GECO assiste la formalisation d’une stratégie environnementale adaptée aux profils de maturité des fournisseurs. La méthode a été expérimentée en milieu industriel au cours de deux cas d’étude réalisées, pour l’un, chez un grand systémier du secteur ferroviaire et, pour l’autre, avec le concours d’une petite entreprise du secteur de la défense. La pertinence de la méthode a ainsi été confirmée, notamment en ce qui concerne la partie diagnostic. / The increase of the environmental issues drives to the integration of the environmental dimension in the product design process of companies of the mechanical industry. This process has widely evolved for the last decades, since suppliers are more deeply involved into their clients' process. As they reach a high level of responsibility, they may heavily influence the product environmental performance of a final system. Hence it is required to improve the integration of the environment in the client/supplier relationship. This integration is however limited due to three main issues : (1) an organizational issue linked the low integration of the environment in corporate hierarchical levels, (2) an operational issue which refers to the reduced environmental expertise which limits the long-term integration of the environment in the product design process, (3) a relational issue which concerns the unbalanced relationship between clients and suppliers. Our research work leads to the method GECO (Management of the Environment in the Client/Supplier relationship). It supports mechanical companies though a consistent, pro-active and tailor made approach within the management of the environment with clients and suppliers. First, the method allows companies to visualize the growing clients’ environmental issues they would potentially have to face up in short and long term. Thus it provides strategic information to focus the efforts on the relevant environmental issues. Second, the method provides a roadmap which guides companies with the choice of the relevant methods and tools to respond to the clients’ requirements. Finally, the method GECO supports the elaboration of an environmental strategy adapted to the suppliers' maturity. The method was experimented though two study cases with a large company from the railway industry and a small company of the defense sector. The relevance of the method has been confirmed, especially the diagnosis part.

De nos jours, les workflows sont largement utilisés par les entreprises et les organisations en vue d’améliorer l’efficacité organisationnelle, la réactivité et la rentabilité en gérant les tâches et les étapes de processus opérationnels. La vérification des spécifications est devenue obligatoire afin d’assurer que ces processus sont correctement conçus et atteignent le niveau de confiance et de qualité attendu.Dans ce contexte, cette thèse porte sur la vérification de spécifications modales – comportements nécessaires ou recevables impliquant plusieurs activités et leurs causalités – de workflows nets – une classe de réseaux de Petri adaptés à la description de workflows. En particulier, cette thèse définit un cadre novateur permettant de modéliser les exécutions de workflow nets,avec ou sans données, et de vérifier des spécifications modales à l’aide de systèmes de contraintes. Elle présente également deux méthodes de réduction préservant la "generalised soundness" et la validité d’une spécification modale donnée. Ces méthodes de réduction sont ensuite présentées comme des étapes de prétraitement réduisant la taille des workflow nets, de sorte que la vérification des propriétés conservées puisse être effectuée sur de plus petites instances. Enfin, cette thèse présente les outils qui ont été mis en oeuvre ainsi que des expérimentations qui ont été menées sur un grand nombre de workflows industriels afin de valider les approches proposées dans cette thèse. Ces résultats expérimentaux convaincants mettent en évidence l’efficacité, l’efficience et le passage à l’échelle de la méthode vérification de spécification modales ainsi que des méthodes de réduction introduites dans cette thèse. / Nowadays workflows are extensively used by companies and organisations in order to improve organizationaleffciency, responsiveness and profitability by managing the tasks and steps of business processes. Theverification of specifications has become mandatory to ensure that such processes are properly designedand reach the expected level of trust and quality. In this context, this thesis addresses the verification ofmodal specifications – necessary or admissible behaviour involving several activities and their causalities –of workflow nets – a Petri nets class suited for the description of workflows.In particular, it defines an innovative constraint system based framework to model executions of ordinary as wellas coloured workflow nets, and verify modal specifications. Further, it presents powerful reduction methodspreserving properties of interest such as generalised soundness and correctness of a given modal specification.Such reduction methods are then portrayed as pre-processing steps reducing workflow nets size, so that theverification of preserved properties can be carried out on smaller instances.Finally, as a practical contribution, this thesis introduces the tools that have been implemented as well asexperimentations that have been carried out over industrial workflow nets in order to validate the approachesproposed in this thesis. The convincing experimental results highlight the effectiveness, effciency andscalability of the modal specification verification method and reduction methods introduced in this thesis.