L'avantage majeur qu'offrent les services Web est le fait qu'ils reposent sur des standards et les technologies du Web pour interagir en s'échangeant des messages. A part les séquences de messages, d'autres facteurs affectent l'interopérabilité des services Web, telles que les contraintes temporelles qui spécifient les délais nécessaires pour échanger des messages. La thèse rapportée dans ce manuscrit étudie l'impact de ces propriétés dans la composition de services Web. La considération de telles propriétés soulève plusieurs problèmes auxquels on a essayé d'apporter une solution. Le premier aspect consiste à définir un modèle qui tienne compte des abstractions nécessaires afin de pouvoir analyser et synthétiser une composition, à savoir les messages, les données, les contraintes de données, les propriétés temporelles et l'aspect asynchrone des communications des services. En se basant sur ce modèle, le deuxième problème consiste à proposer une approche d'analyse de compatibilité. Cette analyse vise à caractériser la compatibilité ou la non-compatibilité des services Web et ce en prenant en considération les abstractions précédemment citées. Nous étudions particulièrement l'impact des propriétés temporelles dans une chorégraphie dans laquelle les services Web supportent des communications asynchrones. Nous proposons une démarche basée sur le model checking qui permet de détecter les éventuels conflits temporisés qui peuvent surgir dans une chorégraphie. Finalement, le dernier problème auquel nous nous intéressons est celui de la construction d'une composition qui essaie de répondre au besoin du client et ce en prenant en compte les aspects temporels. L'approche que l'on propose est basée sur la génération d'un médiateur pour essayer, quand c'est possible, de contourner les incompatibilités temporisées et non-temporisées qui peuvent surgir lors d'une collaboration. Des mécanismes et des algorithmes ont été développés afin de mettre en oeuvre ces objectifs.

Les systèmes fonctionnant sur un réseau ouvert tels que les bases de données médicales ou les systèmes bancaires peuvent manipuler des informations dont la confidentialité doit être impérativement préservée. Dans ce contexte, la notion d'opacité formalise la capacité d'un système à garder secrètes certaines informations critiques. Dans cette thèse, nous nous intéressons à la fois à vérifier que la propriété d'opacité est satisfaite et à la synthèse de systèmes opaques. Vérifier l'opacité est un problème décidable pour des systèmes de transition finis. Pour les systèmes infinis, nous étudions l'application de techniques d'interprétation abstraite à la détection de vulnérabilité. Nous présentons aussi une méthode alternative qui s'appuie sur des abstractions régulières et sur des techniques de diagnostique pour détecter de telles vulnérabilité à l'exécution du système. Pour la synthèse de système opaque, nous appliquons dans un premier temps la théorie du contrôle à la Ramadge et Wonham pour calculer un contrôleur assurant l'opacité. Nous montrons que les techniques habituelles de synthèse de contrôleur ne peuvent être appliqué pour ce problème d'opacité et nous développons alors de nouveaux algorithmes pour calculer l'unique système opaque qui soit maximal au sens de l'inclusion des langages. Ces résultats sont à rapprocher des techniques de construction de système sécurisé par assemblage de composant. Finalement, nous présentons une autre approche pour la synthèse de système opaque qui consiste à synthétiser un filtre qui décide, dynamiquement, de masquer des événements observable afin d'éviter que de l'information secrète ne soit révélée. Ceci permet d'étudier dans un cadre formel la synthèse automatique de pare-feu assurant la confidentialité de certaines informations critiques.

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour la sécurité : ils en contrôlent l'exécution afin que celles-ci se comportent de manière sûre dans le contexte d'un environnement dont l'évolution peut être imprévisible. Un STR n'a d'autre alternative que de s'adapter `a son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier. Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté à la description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelques tâches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe. En premier lieu, la modélisation efficace d'une gamme étendue de politiques d'ordonnancements se heurte à l'incapacité des RdPT à imposer un ordre d'apparition à des évènements concurrents survenant au même instant. D'autre part, les STR ont une nette tendance à être constitués de caract éristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guère adaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deux problèmes, nous proposons dans cette thèse Cifre - en partenariat entre Airbus et le Laas-Cnrs - d'étendre les RdPT à l'aide de deux nouvelles relations, les relations d'inhibition et de permission, permettant de spécifier de manière plus fine les contraintes de temps. Afin de cerner un périmètre clair d'adéquation de cette nouvelle extension à la modélisation des systèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs : déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporels à inhibitions/permissions et fournir un langage simple à la communauté temps réel dont la vérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L'explorateur d'espace d'états de la boite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola.

Pour modéliser le fonctionnement d'un système, décrire une situation ou représenter des idées, on se met intuitivement à dessiner des bulles et les lier par des flèches sous forme de graphes étiquetés. Les logiques modales constituent un cadre formel expressif et extensible qui permet de définir ces graphes sous forme de « modèles », et d'exprimer certaines propriétés de ces graphes sous forme de « formules » afin de pouvoir raisonner là-dessus: model checking, test de satisfiabilité ou de validité, etc. Pour des formules et modèles de tailles importantes, ces tâches deviennent compliquées. De ce fait, un outil permettant de les réaliser automatiquement s'avère nécessaire. LoTREC en est un exemple. Il permet à son utilisateur de créer sa propre méthode de preuve, grâce à un langage simple et de haut niveau, sans avoir besoin d'aucune expertise spécifique en programmation. Durant ma thèse, j'ai revu le travail qui était déjà accompli dans LoTREC et j'ai apporté de nouvelles extensions qui s'avéraient nécessaires pour pouvoir traiter de nouvelles logiques (K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...) et offrir à l'utilisateur certaines nouvelles techniques. D'autre part, j'ai examiné les origines de LoTREC dans le monde de réécriture de graphes et j'ai spécifié la sémantique de son moteur de réécriture. Cela a permis d'éclaircir comment l'on peut hériter dans nos méthodes de preuve des résultats et des propriétés théoriques déjà bien établies dans le domaine de la réécriture de graphes.

<p>Les travaux présentés portent sur l'étude de méthodes de vérification paramétrée des systèmes temps réels. La motivation pour ces recherches est de proposer des méthodes formelles à appliquer sur des systèmes dont les spécifications ne sont pas encore complètes. Des paramètres sont donc introduits dans les modèles utilisés afin de donner des degrés de liberté à la modélisation. Le but est alors de guider la conception du système en déterminant des valeurs satisfaisantes pour les paramètres.</p> <p>Nous nous sommes focalisé sur les paramètres temporels qui sont en général parmi les plus complexes à définir. Nous avons ainsi défini le modèle des réseaux de Petri à chronomètres paramétrés.</p> <p>Dans une première approche, nous étendons les méthodes d'analyse classiquement utilisées dans les réseaux de Petri temporels. L'espace d'états du modèle paramétré est ainsi représenté par le graphe des classes d'états paramétrées. Cela nous permet de proposer des semi-algorithmes de model-checking paramétré avec lesquels nous vérifions des formules de logique TCTL paramétrées.</p> <p>Dans une seconde approche, nous étudions les méthodes qui préservent le parallélisme des réseaux de Petri. L'intérêt est de limiter l'explosion combinatoire qui apparaît lors de l'analyse de systèmes distribués, en particulier avec des modèles paramétrés. Nous proposons pour cela une méthode de dépliage temporel paramétré. Ce dépliage est a priori infini, mais nous proposons de l'utiliser pour résoudre un problème de supervision. La construction du dépliage est alors guidée par des observations finies, et nous extrayons les explications de ces observations, ainsi que les contraintes sur les paramètres qu'elles induisent.</p>

<p>Nowadays, embedded systems are becoming more and more complex. For this reason, designers focus more and more to adopt component-based methods for their designs. Consequently, there is an increasing interest on modeling and verification issues of component-based embedded systems. </p><p>In this thesis, a tool, which integrates modeling, simulation and verification of component-based embedded systems, is designed and implemented. This tool uses the PRES+, Petri Net based Representation for Embedded Systems, to model component-based embedded systems. Both simulation and verification of systems are based on the PRES+ models. </p><p>This tool consists of three integrated sub-tools, each of them with a graphical interface, the PRES+ Modeling tool, the PRES+ Simulation tool and the PRES+ Verification tool. The PRES+ Modeling tool is a graphical editor, with which system designers can model component-based embedded systems easily. The PRES+ Simulation tool, which is used to validate systems, visualizes the execution of a model in an intuitive manner. The PRES+ Verification tool provides a convenient access to a model checker, in which models can be formally verified with respect to temporal logic formulas.</p>

<p>In recent years, there has been much advancement in the area of verification of infinite-state systems. A system can have an infinite state-space due to unbounded data structures such as counters, clocks, stacks, queues, etc. It may also be infinite-state due to parameterization, i.e., the possibility of having an arbitrary number of components in the system. For parameterized systems, we are interested in checking correctness of all the instances in one verification step. </p><p>In this thesis, we consider systems which contain both sources of infiniteness, namely: (a) real-valued clocks and (b) parameterization. More precisely, we consider two models: (a) the timed Petri net (TPN) model, which is an extension of the classical Petri net model; and (b) the timed network (TN) model in which an arbitrary number of timed automata run in parallel. </p><p>We consider verification of safety properties for timed Petri nets using forward analysis. Since forward analysis is necessarily incomplete, we provide a semi-algorithm augmented with an acceleration technique in order to make it terminate more often on practical examples. Then we consider a number of problems which are generalisations of the corresponding ones for timed automata and Petri nets. For instance, we consider zenoness where we check the existence of an infinite computation with a finite duration. We also consider two variants of boundedness problem: syntactic boundedness in which both live and dead tokens are considered and semantic boundedness where only live tokens are considered. We show that the former problem is decidable while the latter is not. Finally, we show undecidability of LTL model checking both for dense and discrete timed Petri nets. </p><p>Next we consider timed networks. We show undecidability of safety properties in case each component is equipped with two or more clocks. This result contrasts previous decidability result for the case where each component has a single clock. Also ,we show that the problem is decidable when clocks range over the discrete time domain. This decidability result holds when the processes have any finite number of clocks. Furthermore, we outline the border between decidability and undecidability of safety for TNs by considering several syntactic and semantic variants.</p>

This work studies new algorithms and data structures that are useful in the context of program verification. As computers have become more and more ubiquitous in our modern societies, an increasingly large number of computer-based systems are considered safety-critical. Such systems are characterized by the fact that a failure or a bug (computer error in the computing jargon) could potentially cause large damage, whether in loss of life, environmental damage, or economic damage. For safety-critical systems, the industrial software engineering community increasingly calls for using techniques which provide some formal assurance that a certain piece of software is correct. One of the most successful program verification techniques is model checking, in which programs are typically abstracted by a finite-state machine. After this abstraction step, properties (typically in the form of some temporal logic formula) can be checked against the finite-state abstraction, with the help of automated tools. Alternating automata play an important role in this context, since many temporal logics on words and trees can be efficiently translated into those automata. This property allows for the reduction of model checking to automata-theoretic questions and is called the automata-theoretic approach to model checking. In this work, we provide three novel approaches for the analysis (emptiness checking) of alternating automata over finite and infinite words. First, we build on the successful framework of antichains to devise new algorithms for LTL satisfiability and model checking, using alternating automata. These algorithms combine antichains with reduced ordered binary decision diagrams in order to handle the exponentially large alphabets of the automata generated by the LTL translation. Second, we develop new abstraction and refinement algorithms for alternating automata, which combine the use of antichains with abstract interpretation, in order to handle ever larger instances of alternating automata. Finally, we define a new symbolic data structure, coined lattice-valued binary decision diagrams that is particularly well-suited for the encoding of transition functions of alternating automata over symbolic alphabets. All of these works are supported with empirical evaluations that confirm the practical usefulness of our approaches. / Ce travail traite de l'étude de nouveaux algorithmes et structures de données dont l'usage est destiné à la vérification de programmes. Les ordinateurs sont de plus en plus présents dans notre vie quotidienne et, de plus en plus souvent, ils se voient confiés des tâches de nature critique pour la sécurité. Ces systèmes sont caractérisés par le fait qu'une panne ou un bug (erreur en jargon informatique) peut avoir des effets potentiellement désastreux, que ce soit en pertes humaines, dégâts environnementaux, ou économiques. Pour ces systèmes critiques, les concepteurs de systèmes industriels prônent de plus en plus l'usage de techniques permettant d'obtenir une assurance formelle de correction. Une des techniques de vérification de programmes les plus utilisées est le model checking, avec laquelle les programmes sont typiquement abstraits par une machine a états finis. Après cette phase d'abstraction, des propriétés (typiquement sous la forme d'une formule de logique temporelle) peuvent êtres vérifiées sur l'abstraction à espace d'états fini, à l'aide d'outils de vérification automatisés. Les automates alternants jouent un rôle important dans ce contexte, principalement parce que plusieurs logiques temporelle peuvent êtres traduites efficacement vers ces automates. Cette caractéristique des automates alternants permet de réduire le model checking des logiques temporelles à des questions sur les automates, ce qui est appelé l'approche par automates du model checking. Dans ce travail, nous étudions trois nouvelles approches pour l'analyse (le test du vide) desautomates alternants sur mots finis et infinis. Premièrement, nous appliquons l'approche par antichaînes (utilisée précédemment avec succès pour l'analyse d'automates) pour obtenir de nouveaux algorithmes pour les problèmes de satisfaisabilité et du model checking de la logique temporelle linéaire, via les automates alternants.Ces algorithmes combinent l'approche par antichaînes avec l'usage des ROBDD, dans le but de gérer efficacement la combinatoire induite par la taille exponentielle des alphabets d'automates générés à partir de LTL. Deuxièmement, nous développons de nouveaux algorithmes d'abstraction et raffinement pour les automates alternants, combinant l'usage des antichaînes et de l'interprétation abstraite, dans le but de pouvoir traiter efficacement des automates de grande taille. Enfin, nous définissons une nouvelle structure de données, appelée LVBDD (Lattice-Valued Binary Decision Diagrams), qui permet un encodage efficace des fonctions de transition des automates alternants sur alphabets symboliques. Tous ces travaux ont fait l'objet d'implémentations et ont été validés expérimentalement.

La conduite de systèmes autonomes nécessite de prendre des décisions en fonction des observations et des objectifs courants : cela implique des tâches à effectuer en ligne, avec les moyens de calcul embarqués. Cependant, il s'agit généralement de tâches combinatoires, gourmandes en temps de calcul et en espace mémoire. Réaliser ces tâches intégralement en ligne dégrade la réactivité du système ; les réaliser intégralement hors ligne, en anticipant toutes les situations possibles, nuit à son embarquabilité. Les techniques de compilation de connaissances sont susceptibles d'apporter un compromis, en déportant au maximum l'effort de calcul avant la mise en situation du système. Ces techniques consistent à traduire un problème dans un certain langage, fournissant une forme compilée de ce problème, dont la résolution est facile et la taille aussi compacte que possible. L'étape de traduction peut être très longue, mais elle n'est effectuée qu'une seule fois, hors ligne. Il existe de nombreux langages-cible de compilation, notamment le langage des diagrammes de décision binaires (BDDs), qui ont été utilisés avec succès dans divers domaines de l'intelligence artificielle, tels le model-checking, la configuration ou la planification. L'objectif de la thèse était d'étudier l'application de la compilation de connaissances à la conduite de systèmes autonomes. Nous nous sommes intéressés à des problèmes réels de planification, qui impliquent souvent des variables continues ou à grand domaine énuméré (temps ou mémoire par exemple). Nous avons orienté notre travail vers la recherche et l'étude de langages-cible de compilation assez expressifs pour permettre de représenter de tels problèmes. Dans la première partie de la thèse, nous présentons divers aspects de la compilation de connaissances ainsi qu'un état de l'art de l'utilisation de la compilation dans le domaine de la planification. Dans une seconde partie, nous étendons le cadre des BDDs aux variables réelles et énumérées, définissant le langage-cible des " interval automata " (IAs). Nous établissons la carte de compilation des IAs et de certaines restrictions des IAs, c'est-à-dire leurs propriétés de compacité et leur efficacité vis-à-vis d'opérations élémentaires. Nous décrivons des méthodes de compilation en IAs pour des problèmes exprimés sous forme de réseaux de contraintes continues. Dans une troisième partie, nous définissons le langage-cible des " set-labeled diagrams " (SDs), une autre généralisation des BDDs, permettant de représenter des IAs discrétisés. Nous établissons la carte de compilation des SDs et de certaines restrictions des SDs, et décrivons une méthode de compilation de réseaux de contraintes discrets en SDs. Nous montrons expérimentalement que l'utilisation de IAs et de SDs pour la conduite de systèmes autonomes est prometteuse.

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components. At the same time, the systems must fulfill strict functional and non-functional requirements. This thesis presents novel and efficient techniques for the verification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+. Two complementary problems are addressed: component verification and integration verification. With component verification the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment. Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of SystemC designs by translating them into the PRES+ representation. The second technique involves a simulation based approach into which formal methods are injected to boost verification efficiency. Provided that each individual component is verified and is guaranteed to function correctly, the components are interconnected to form a complete system. What remains to be verified is the interface logic, also called glue logic, and the interaction between components. Each glue logic and interface cannot be verified in isolation. It must be put into the context in which it is supposed to work. An appropriate environment must thus be derived from the components to which the glue logic is connected. This environment must capture the essential properties of the whole system with respect to the properties being verified. In this way, both the glue logic and the interaction of components through the glue logic are verified. The thesis presents algorithms for automatically creating such environments as well as the underlying theoretical framework and a step-by-step roadmap on how to apply these algorithms.