Le présent mémoire propose une investigation approfondie de l’analyseur Alloy afin de juger son adaptabilité en tant que vérificateur de modèles. Dans un premier temps, l’étude dresse un tableau comparatif de six vérificateurs de modèles, incluant Alloy, afin de déterminer lequel d’entre eux est le plus apte à résoudre les problématiques de sécurité fonctionnelle posées par les systèmes d’information. En conclusion de cette première phase, Alloy émerge comme l’un des analyseurs les plus performants pour vérifier les modèles sur lesquels se fondent les systèmes d’information. Dans un second temps, et sur la base des problématiques rencontrées au cours de cette première phase, l’étude rapporte une série d’idiomes pour, d’une part, présenter une manière optimisée de spécifier des traces et, d’autre part, trouver des recours afin de contourner les limitations imposées par Alloy. À ces fins, le mémoire propose deux nouveaux cas d’espèce, ceux d’une cuisinière intelligente et d’une boîte noire, afin de déterminer si oui ou non l’analyseur est capable de gérer les systèmes dynamiques possédant de nombreuses entités avec autant d’efficacité que les systèmes qui en possèdent moins. En conclusion, le mémoire rapporte que Alloy est un bon outil pour vérifier des systèmes dynamiques mais que sa version récente, DynAlloy, peut être encore mieux adapté pour le faire puisque précisément conçu pour faire face aux spécificités de ce type de système. Le mémoire s’achève sur une présentation sommaire de ce dernier outil.

Les systèmes cyber-physiques mélangent des comportements physiques continus, tel la vitesse d'un véhicule, et des comportement discrets, tel que le régulateur de vitesse d'un véhicule. Ils sont désormais omniprésents dans notre société. Un grand nombre de ces systèmes sont dits critiques, i.e. une mauvaise conception entraînant un comportement non prévu, un bug, peut mettre en danger des êtres humains. Il est nécessaire de développer des méthodes pour garantir le bon fonctionnement de tels systèmes. Les méthodes formelles regroupent des procédés mathématiques pour garantir qu'un système se comporte comme attendu, par exemple que le régulateur de vitesse n'autorise pas de dépasser la vitesse maximale autorisée. De récents travaux ont permis des progrès significatifs dans ce domaine, mais l'approche adoptée est encore monolithique, i.e. que le système est modélisé d'un seul tenant et est ensuite soumis à la preuve. Notre problématique est comment modéliser efficacement des systèmes cyber-physiques dont la complexité réside dans une répétition de morceaux élémentaires. Et une fois que l'on a obtenu une modélisation, comment garantir le bon fonctionnement de tels systèmes. Notre approche consiste à modéliser le système de manière compositionnelle. Plutôt que de vouloir le modéliser d'un seul tenant, il faut le faire morceaux par morceaux, appelés composants. Chaque composant correspond à un sous-système du système final qu'il est simple de modéliser. On obtient le système complet en assemblant les composants ensembles. Ainsi une usine de traitement des eaux est obtenue en assemblant différentes cuves. L'intérêt de cette méthode est qu'elle correspond à l'approche des ingénieurs dans l'industrie : considérer des éléments séparés que l'on compose ensuite. Mais cette approche seule ne résout pas le problème de la preuve de bon fonctionnement du système. Il faut aussi rendre la preuve compositionnelle. Pour cela, on associe à chaque composant des propriétés sur ses entrées et sortie, et on prouve qu'elles sont respectées. Cette preuve peut être effectué par un expert, mais aussi par un ordinateur si les composants sont de tailles raisonnables. Il faut ensuite nous assurer que lors de l'assemblage des composants, les propriétés continuent à être respectées. Ainsi, la charge de la preuve est reportée sur les composants élémentaires, l'assurance du respect des propriétés désirées est conservée lors des étapes de composition. On peut alors obtenir une preuve du bon fonctionnement de systèmes industriels avec un coût de preuve réduit. Notre contribution majeure est de proposer une telle approche compositionnelle à la fois pour modéliser des systèmes cyber-physiques, mais aussi pour prouver qu'ils respectent les propriétés voulues. Ainsi, à chaque étape de la conception, on s'assure que les propriétés sont conservées, si possible à l'aide d'un ordinateur. Le système résultant est correct par construction. De ce résultat, nous avons proposé plusieurs outils pour aider à la conception de systèmes cyber-physiques de manière modulaire. On peut raisonner sur les propriétés temporelles de tels systèmes, par exemple est-ce que le temps de réaction d'un contrôleur est suffisamment court pour garantir le bon fonctionnement. On peut aussi raisonner sur des systèmes où un mode nominal cohabite avec un mode d'urgence. / Cyber-physical systems mix continuous physical behaviors, e.g. the velocity of a vehicle, and discrete behaviors, e.g. the cruise-controller of the vehicle. They are pervasive in our society. Numerous of such systems are safety-critical, i.e. a design error which leads to an unexpected behavior can harm humans. It is mandatory to develop methods to ensure the correct functioning of such systems. Formal methods is a set of mathematical methods that are used to guarantee that a system behaves as expected, e.g. that the cruise-controller does not allow the vehicle to exceed the speed limit. Recent works have allowed significant progress in the domain of the verification of cyber-physical systems, but the approach is still monolithic. The system under consideration is modeled in one block. Our problematic is how to efficiently model cyber-physical systems where the complexity lies in a repetition of elementary blocks. And once this modeling done, how guaranteeing the correct functioning of such systems. Our approach is to model the system in a compositional manner. Rather than modeling it in one block, we model it pieces by pieces, called components. Each component correspond to a subsystem of the final system and are easier to model due to their reasonable size. We obtain the complete system by assembling the different components. A water-plant will thus be obtained by the composition of several water-tanks. The main advantage of this method is that it corresponds to the work-flow in the industry : consider each elements separately and compose them later. But this approach does not solve the problem of the proof of correct functioning of the system. We have to make the proof compositional too. To achieve it, we associate to each component properties on its inputs and outputs, then prove that they are satisfied. This step can be done by a domain expert, but also by a computer program if the component is of a reasonable size. We have then to ensure that the properties are preserved through the composition. Thus, the proof effort is reported to elementary components. It is possible to obtain a proof of the correct functioning of industrial systems with a reduced proof effort. Our main contribution is the development of such approach in Differential Dynamic Logic. We are able to modularly model cyber-physical systems, but also prove their correct functioning. Then, at each stage of the design, we can verify that the desired properties are still guaranteed. The resulting system is correct-by-construction. From this result, we have developed several tools to help for the modular reasoning on cyber-physical systems. We have proposed a methodology to reason on temporal properties, e.g. if the execution period of a controller is small enough to effectively regulate the continuous behavior. We have also showed how we can reason on functioning modes in our framework.

L'objectif principal de cette thèse est de définir un langage logique de haut niveau qui permet l'expression de politiques de sécurité complexes au sein d'un modèle de contrôle d'accès. Le développement de ce langage se fait en trois temps. Dans un premier temps nous présentons un modèle dynamique basé sur les rôles. Ainsi, nous considérons que l'évolution de l'état de sécurité d'un service dépend de l'exécution de ses fonctionnalités. Dans un deuxième temps nous définissons un formalisme basé sur les attributs qui offre plus de flexibilité en termes de spécifications des conditions de contrôle d'accès, et ajoutons la notion de workflow qui permet de modéliser le comportement d'un service. Dans un dernier temps, nous ajoutons un mécanisme de négociation qui permet à chaque service de définir sa propre politique d'échange avec les autres services dans l'environnement. La conception d'un tel cadre logique unifié facilite l'analyse de sûreté des politiques de sécurité puisque tous les facteurs qui influencent les décisions de contrôle d'accès sont pris en compte dans le même cadre. Ainsi le second objectif de cette thèse est d'étudier d'une part les principales propriétés de contrôle d'accès tels la délégation et la séparation des tâches et d'autre part les propriétés de sécurité pour la communication entre les différents services au niveau de la négociation.

Les concepts d'action et de ressource sont omniprésents en informatique. La caractéristique principale d'une action est de changer l'état actuel du système modélisé. Une action peut ainsi être l'exécution d'une instruction dans un programme, l'apprentissage d'un fait nouveau, l'acte concret d'un agent autonome, l'énoncé d'un mot ou encore une tâche planifiée. La caractéristique principale d'une ressource est de pouvoir être divisée, par exemple pour être partagée. Il peut s'agir des cases de la mémoire d'un ordinateur, d'un ensemble d'agents, des différent sens d'une expression, d'intervalles de temps ou de droits d'accès. Actions et ressources correspondent souvent aux dimensions temporelles et spatiales du système modélisé. C'est le cas par exemple de l'exécution d'une instruction sur une case de la mémoire ou d'un groupe d'agents qui coopèrent. Dans ces cas, il est possible de modéliser les actions parallèles comme étant des actions opérant sur des parties disjointes des ressources disponibles. Les logiques modales permettent de modéliser les concepts d'action et de ressource. La sémantique relationnelle d'une modalité unaire est une relation binaire permettant d'accéder à un nouvel état depuis l'état courant. Ainsi une modalité unaire correspond à une action. De même, la sémantique d'une modalité binaire est une relation ternaire permettant d'accéder à deux états. En considérant ces deux états comme des sous-états de l'état courant, une modalité binaire modélise la séparation de ressources. Dans cette thèse, nous étudions des logiques modales utilisées pour raisonner sur les actions, les ressources et la concurrence. Précisément, nous analysons la décidabilité et la complexité du problème de satisfaisabilité de ces logiques. Ces problèmes consistent à savoir si une formule donnée peut être vraie. Pour obtenir ces résultats de décidabilité et de complexité, nous proposons des procédures de décision. Ainsi, nous étudions les logiques modales avec des modalités binaires, utilisées notamment pour raisonner sur les ressources. Nous nous intéressons particulièrement à l'associativité. Alors qu'il est généralement souhaitable que la modalité binaire soit associative, puisque la séparation de ressources l'est, cette propriété rend la plupart des logiques indécidables. Nous proposons de contraindre la valuation des variables propositionnelles afin d'obtenir des logiques décidables ayant une modalité binaire associative. Mais la majeure partie de cette thèse est consacrée à des variantes de la logique dynamique propositionnelle (PDL). Cette logiques possède une infinité de modalités unaires structurée par des opérateurs comme la composition séquentielle, l'itération et le choix non déterministe. Nous étudions tout d'abord des variantes de PDL comparables aux logiques temporelle avec branchement. Nous montrons que les problèmes de satisfaisabilité de ces variantes ont la même complexité que ceux des logiques temporelles correspondantes. Nous étudions ensuite en détails des variantes de PDL ayant un opérateur de composition parallèle de programmes inspiré des logiques de ressources. Cet opérateur permet d'exprimer la séparation de ressources et une notion intéressante d'actions parallèle est obtenue par la combinaison des notions d'actions et de séparation. En particulier, il est possible de décrire dans ces logiques des situations de coopération dans lesquelles une action ne peut être exécutée que simultanément avec une autre. Enfin, la contribution principale de cette thèse est de montrer que, dans certains cas intéressants en pratique, le problème de satisfaisabilité de ces logiques a la même complexité que PDL. / The concepts of action and resource are ubiquitous in computer science. The main characteristic of an action is to change the current state of the modeled system. An action may be the execution of an instruction in a program, the learning of a new fact, a concrete act of an autonomous agent, a spoken word or a planned task. The main characteristic of resources is to be divisible, for instance in order to be shared. Resources may be memory cells in a computer, performing agents, different meanings of a phrase, time intervals or access rights. Together, actions and resources often constitute the temporal and spatial dimensions of a modeled system. Consider for instance the instructions of a computer executed at memory cells or a set of cooperating agents. We observe that in these cases, an interesting modeling of concurrency arises from the combination of actions and resources: concurrent actions are actions performed simultaneously on disjoint parts of the available resources. Modal logics have been successful in modeling both concepts of actions and resources. The relational semantics of a unary modality is a binary relation which allows to access another state from the current state. Hence, unary modalities are convenient to model actions. Similarly, the relational semantics of a binary modality is a ternary relation which allows to access two states from the current state. By interpreting these two states as substates of the current state, binary modalities allow to divide states. Hence, binary modalities are convenient to model resources. In this thesis, we study modal logics used to reason about actions, resources and concurrency. Specifically, we analyze the decidability and complexity of the satisfiability problem of these logics. These problems consist in deciding whether a given formula can be true in any model. We provide decision procedures to prove the decidability and state the complexity of these problems. Namely, we study modal logics with a binary modality used to reason about resources. We are particularly interested in the associativity property of the binary modality. This property is desirable since the separation of resources is usually associative too. But the associativity of a binary modality generally makes the logic undecidable. We propose in this thesis to constrain the valuation of propositional variables to make modal logics with an associative binary modality decidable. The main part of the thesis is devoted to the study of variants of the Propositional Dynamic Logic (PDL). These logics features an infinite set of unary modalities representing actions, structured by some operators like sequential composition, iteration and non-deterministic choice. We first study branching time variants of PDL and prove that the satisfiability problems of these logics have the same complexity as the corresponding branching-time temporal logics. Then we thoroughly study extensions of PDL with an operator for parallel composition of actions called separating parallel composition and based on the semantics of binary modalities. This operator allows to reason about resources, in addition to actions. Moreover, the combination of actions and resources provides a convenient expression of concurrency. In particular, these logics can express situations of cooperation where some actions can be executed only in parallel with some other actions. Finally, our main contribution is to prove that the complexity of the satisfiability problem of a practically useful variant of PDL with separating parallel composition is the same as the satisfiability problem of plain PDL.