Ces travaux de recherche ont été réalisés dans le cadre du projet régional Com-SLoT (Communauté de Services Logistiques sur l'Internet des Objets) qui s'inscrit dans l'axe des "outils numériques pour la performance industrielle" (2013-2016). Com-SLoT vise à mettre en place une communauté de services pour la gestion des objets logistiques. Il s'agit précisément de récolter et de partager toutes les informations nécessaires à la planification, l'exécution et la coordination des flux. Le problème qui est posé dans cette thèse est la "Modélisation des flux logistiques : vers une plate-forme d'interopérabilité des objets logistiques". Le modèle de flux de marchandises que nous cherchons à modéliser a donc pour objectif et défi principal de faciliter le développement et la mise en place des systèmes de gestion collaboratives de flux de marchandises basés sur l'Internet des objets et les plateformes cloud Computing. Ce défi scientifique et technologique peut se décliner en sous objectifs comme suit : (1) Proposer un modèle générique de flux logistique centré sur l'entité logistique en tant qu'entité autonome et communicante. (2) Passer de l’échange au partage : Collecter les données sur l'entité et le flux logistique, stocker et partager ces données à l'ensemble des acteurs de la supply chain. (3) Gérer l'hétérogénéité des données et les droits d'accès pour l'interopérabilité des flux. (4) Intégrer le flux de marchandises avec les technologies de l'internet des objets et des plateformes Cloud. (5) Réaliser une vrai plateforme collaborative en mode SaaS : dans ce cadre, il est plus question d'architecture et d'intégration / This research project was carried out within the framework of the regional project COM-SLoT (Community of Logistics Services on the Internet of Things). This project is in the field of "Digital tools for industrial performance". COM-SLoT aims to set up a community of services for the management of logistics workflows and related business entities. It is a matter of collecting and sharing all information necessary for the planning, the execution and the coordination of workflows. The problem to solve in this thesis is the "Modeling of logistic flows : towards a platform for business entities interoperability". The workflow model we are going to seek therefore has as main goal and challenges to facilitate the design of collaborative management of workflows, based on Internet of Things and Cloud Computing technologies. This challenge can be broken down into sub-goals as follows : (1) Propose a generic workflow model focused on the logistics entity as an autonomous and communicating entity. (2) Switching from peer to peer (PoP) data exchange to information sharing : collecting data on entities and workflows, storing and sharing to supply chain stakeholders. (3) Manage data heterogeneity and access rights to enable workflow interoperability. (4) Integrate Internet of Things technologies in the business entities. (5) Design a SaaS based collaborative platform to overcome existing architectural failures

Les travaux de cette thèse s'inscrivent dans le cadre de la vérification des logiciels et plus particulièrement du test à partir de spécifications algébriques. La soumission d'un jeu de tests exhaustif pour trouver toutes les erreurs d'un programme est généralement impossible. Il faut donc sélectionner un jeu de tests le plus judicieusement possible. Nous avons donc donné une méthode de sélection de tests par dépliage des axiomes de spécifications conditionnelles positives (clauses de Horn pour la logique équationnelle). Celle-ci permet de partitionner le jeu exhaustif des tests. Nous utilisons pour cela un critère de sélection qui utilise les axiomes de la spécification et qui peut être appliqué plusieurs fois de suite. Pour garantir de bonnes propriétés sur ce critère de sélection, nous avons également donné un cadre général pour la normalisation d'arbre de preuve. Il fonctionne pour n'importe quel système formel, et permet d'unifier un grand nombre de résultats en logique.

Les notations semi-formelles et formelles semblant complémentaires, leur couplage semble un cadre intéressant pour pouvoir bénéficier de leurs avantages respectifs tout en diminuant leurs points faibles. En effet, d'une part, les notations semi-formelles qui pêchent par leur précision sont de bons vecteurs de communication dont le coût de formation est raisonnable ; d'autre part, les langages formels apportent la précision et le potentiel de raisonnement manquant aux notations semi-formelles. Dans ce travail, nous proposons une approche de traduction de modèles semi-formels objet en des spécifications formelles en Z ou en Object-Z afin de fournir un couplage bénéfique de ces deux types de spécifications. Nous cherchons à rendre nos propositions les plus utilisables possible en en montrant trois bénéfices avérés : un guide méthodologique pour l'expression des contraintes annotant un modèle objet, une aide à la vérification des modèles et de leurs contraintes et des raisonnements informels sur la sémantique de modèles simples. Nous avons aussi développé un outil de support à notre approche, RoZ qui permet de faire cohabiter les notations semi-formelles et formelles. Enfin nous étudions une autre approche de couplage, la vérification de cohérence par méta-modélisation pour laquelle nous proposons des règles de cohérence entre le modèle objet et Z. Ce travail nous permet de comparer cette approche avec notre stratégie de traduction afin de mieux comprendre leurs avantages et leurs inconvénients.

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette thèse sous l'angle de la mise en œuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions, la solution actuellement privilégiée dans l'industrie. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette Thèse sous l'angle de la mise en oeuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette Thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système.

La performance d'un projet de conception de produits manufacturés est souvent caractérisée par un ensemble d'indicateurs qui ne repose pas uniquement sur la performance du produit mais sur celle du triptyque produit processus et organisation (PPO). L’utilisation d’indicateurs de performance dans un projet de conception ne peut être efficace que si les liens de traçabilité entre les données sont formalisés. Durant le cycle de conception, de très nombreuses spécifications PPO, également appelées spécifications projet, sont déployées dans un environnement de conception collaborative. Ce déploiement consiste à transférer les spécifications de niveaux de détail donnés vers des niveaux de détail plus affinés (transfert interniveaux) et depuis des vues globales vers des vues particulières (transfert intervues). Ce travail propose de caractériser ces deux mécanismes de transferts, déjà introduits pour les spécifications géométriques, à l’ensemble des spécifications projet. La formalisation et la généralisation de ces mécanismes de transferts ont été identifiées pour un ensemble de modèles pour la conception collaborative (un modèle produit, deux modèles processus (un pour le système décisionnel et un pour le système technologique) et un modèle organisation). Ces modèles constituent ainsi un environnement PPO. Le système décisionnel et le système technologique y sont décrits comme deux aspects du système de conception : l’un s’intéressant à l’organisation et aux processus, l’autre travaillant sur le produit même au travers d’un processus de conception. Les transferts de spécifications y sont ainsi illustrés. La mise en place de perturbations dans un scénario de conception de turbine haute pression permet de mettre en évidence les liens de traçabilité entre les spécifications ainsi que les impacts des perturbations et des solutions censés les corriger. Un indicateur de performance énergétique ayant été défini, des perturbations sont simulées et des solutions sont proposées. La notion de compromis apparaît alors lorsque les solutions améliorent une caractéristique de l’indicateur de performance énergétique mais en dégrade une autre. / Design project performance of manufactured products is often characterised by a set of indicators which does not depend only on the product’s performance but also on that of the product process and organisation (PPO) triptych. The use of performance indicators in a design project can only be effective if the traceability links between the data are formalised. During the design cycle, a lot of PPO specifications, also called project specifications, are deployed in a collaborative design environment. This deployment consists in transferring the specifications from a given detail level towards finer ones (interlevel transfer) and from a global view towards particular ones (interview transfer). This work proposes to characterise these two mechanisms of transfers, already introduced for geometrical specifications, with the whole of project specifications. The formalisation and the generalisation of these mechanisms of transfers were identified for a set of models for collaborative design (one product model, two process models (one for the decision-making system and one for the technological system) and one organisation model). These models provide thus a PPO environment. The decision-making system and the technological system are described there as two aspects of design system: one concerned with the organisation and the processes, the other working on the product through a design process. Specifications transfers are thus illustrated there. The introduction of disturbances in a design scenario of a high-pressure turbine can highlight the traceability links between specifications and the impacts of the disturbances and the solutions to correct them. An energetic performance indicator has been defined, disturbances are simulated and solutions are proposed. The compromise notion appears then when the solutions go better a characteristic of the energetic performance indicator but degrade another one.

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette thèse sous l'angle de la mise en œuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions, la solution actuellement privilégiée dans l'industrie. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système / Nowadays information systems are, more than ever, available through Web browsers. Therefore, they become vulnerable against attack, which has made security an important issue for public and private organizations. This thesis examines in depth one aspect of information system security, namely functional security through access-control policy enforcement, when such systems are implemented in a service-oriented architecture framework. The foundation of the proposed solution is a generic model that introduces essential concepts to design enforcement managers for access-control policies and clearly separates responsibilities between the information system and access control mechanisms. Instantiation of this model results in a general framework, which encompasses many components including a dynamic access-control filter. This thesis also presents two systematic implementation methods for the dynamic access-control filter from policies expressed in ASTD, a formal and graphical notation based on statecharts enriched with process algebra operators. The ASTD notation is more expressive than the RBAC standard and its extensions, the widely used solution in software engineering. The first method is based on the transformation of access-control policies, instantiated from ASTD patterns, into BPEL processes. The second method is based on the interpretation of ASTD specifications by BPEL processes. In these two cases, the BPEL processes are deployed and executed in a BPEL engine, and interact with the information system. Both methods allow for automatic implementation of an enforcement framework from the initial specification. Finally, prototypes have been developed to illustrate both methods and show their feasibility at the functional level and their performance

Pour s'assurer que les personnes âgées soient en sécurité au domicile, le projet INOVUS s'intéresse aux risques liés à l'utilisation de la cuisinière. Dans le cadre de ce projet, les travaux de M.Sc. présentés dans ce mémoire se concentrent sur la perspective logicielle de la détection et de la prévention des risques physiques pour la personne, lors de la réalisation de tâches utilisant la cuisinière. Dans un premier temps, une revue des risques à domicile recensés dans la littérature a permis de définir la couverture nécessaire à une telle solution. Certaines situations dangereuses ont ensuite été sélectionnées pour définir un modèle de solution satisfaisant. Le développement d'une solution de sécurité pour la personne entraîne des contraintes de fiabilité de très haut niveau pour la technologie produite.Pour répondre à ce besoin, la proposition de ces travaux de M.Sc. est l'utilisation de spécifications formelles. Ces outils permettent d'obtenir un plus haut degré de fiabilité de logiciels. En se basant sur ces outils, un modèle de solution a été élaboré pour le projet INOVUS, et ce à l'aide du vérificateur de modèle ALLOY. Enfin, une implémentation en Java de ce prototype a été réalisée afin d'évaluer les résultats de détection des situations dangereuses. Ce prototype permet alors à la fois de valider l'approche de développement choisie, ainsi que d'établir une preuve de concept d'une telle solution de sécurité.

Cette étude a pour but la conversion des spécifications géométriques de tolérance en zones d'incertitudes. Pour cela, une représentation des zones de tolérance a été faite, en tenant compte de tous les différents types de tolérancements pouvant y être imposés. Après cela, ces zones de tolérances ont été exprimées sous forme de torseurs de petits déplacements. Par la suite, les éléments de ces torseurs ont été bornés afin de délimiter la zone de tolérance. À ce stade, les équations gouvernant la conversion des spécifications géométriques en zones d'incertitudes sont établies.Cette procédure a été faite pour chaque type de zone de tolérance à savoir, un disque, un trou, le décalage d'une ligne, le décalage d'une paroi plane, un cylindre, un anneau, un parallélépipède et une rainure. Ce développement a aussi été enlisé pour les deux mouvements de recherche, à savoir les déterministes et les statisticiens. Finalement le principe du maximum de matière a été introduit pour toutes les équations.

Concevoir et mettre en oeuvre des méthodes pour la spécification, l'analyse et la vérification de logiciels et de systèmes sont les principaux moteurs des activités de recherche présentées dans ce manuscrit. Dans ce cadre, nos travaux se positionnent dans la catégorie dite des méthodes formelles appartenant à la communauté plus large du génie logiciel. A l'interface des travaux théoriques et applicatifs, notre objectif est de contribuer aux méthodes permettant d'assurer la correction et la sûreté des systèmes (fonctionnalité, sécurité, fiabilité, ...) en développant ou en améliorant des langages de spécification, des techniques et des outils permettant leur analyse formelle. Dans ce but, nous nous sommes attaché dans cette thèse à proposer et à étudier un cadre formel permettant la définition de politiques de sécurité et la vérification de leurs propriétés. A cet effet, nous avons proposé un cadre pour la spécification de politiques de sécurité basé sur une approche modulaire dans laquelle une politique est vue comme la composition d'un modèle de sécurité et d'une configuration. Nous avons investigué les possibilités offertes par de telles spécifications lorsque les modèles sont exprimés au moyen de contraintes du premier ordre et les configurations au moyen de programmes logiques. En particulier, nous avons proposé un algorithme permettant de transformer une politique exprimée dans un modèle donné vers une autre politique équivalente (au sens où elle engendre les mêmes autorisations) exprimée dans un autre modèle. Dans un second temps, nous nous sommes proposé de tenir compte des aspects dynamiques de la configuration d'une politique vue comme un état du système sur lequel la politique est mise en oeuvre et où chaque action est associée à une procédure de modification des états. Nous avons proposé un langage formel simple pour spécifier séparément les systèmes et les politiques de sécurité puis avons donné une sémantique des spécifications exprimées dans ce cadre sous la forme de systèmes de réécriture. Nous nous sommes ensuite attachés à montrer que les systèmes de réécriture obtenus permettent l'étude de propriétés de sécurité. Dans une troisième partie, nous nous sommes focalisé sur les mécanismes permettant la mise en oeuvre de politiques de sécurité dans les réseaux. Dans ce cadre, nous avons proposé une spécification des firewalls et de leurs compositions basée sur les automates d'arbres et les systèmes de réécriture puis avons montré en quoi ces spécifications nous permettent d'analyser de façon automatique les politiques de sécurité sous-jacentes. / Designing and applying formal methods for specifying, analyzing and verifying softwares and systems are the main driving forces behind the work presented in this manuscript. In this context, our activities fall into the category of formal methods belonging to the wider community of software engineering. At the interface between theoretical and applied research, our aim is to contribute to the methods ensuring the correction and the safety of systems (security, reliability, ...) by developing or by improving specification languages, techniques and tools allowing their formal analysis. In this purpose, we became attached in this thesis to propose and to study a formal framework allowing the specification of security policies and the verification of their properties. We first proposed a framework for specifying security policies based on a modular approach in which policies are seen as a composition of security models and configurations. We investigated the possibilities opened by such specifications when models are expressed by means of first order constraints and configurations by means of logical programs. In particular, we proposed an algorithm allowing the transformation of a security policy expressed in a given model towards another equivalent policy expressed in another model. Secondly, we suggested taking into account dynamic aspects of policy configurations which can be seen as states of the system on which the policy is applied and where each action is associated with a procedure of states modification. We proposed a simple formal language to specify separately systems and security policies and then gave a semantics of specifications expressed in this framework under the form of rewriting systems. We then attempted to show that the obtained rewriting systems allow the analysis of security properties. In the third part, we focused on mechanisms enforcing security policies in networks. In this context, we proposed a specification of firewalls and their compositions based on tree automata and rewriting systems and then showed how these specifications allow us to analyze in an automatic way the underlying security policies.