L'introduction des nouvelles technologies de l'information et de la communication dans les systèmes automatisés entraîne un accroissement de la complexité des fonctions qu'ils supportent. Cet accroissement de la complexité a un impact sur la sécurité des systèmes. En effet, leurs propriétés ne sont plus réductibles aux propriétés de leurs constituants pris isolément mais émergent d'un réseau d'interactions entre ces constituants qui peut être à l'origine de comportements néfastes et difficiles à prévoir. <br />Notre conviction est que le développement sûr de ces systèmes doit combiner des approches pragmatiques orientées " système ", qui tiennent compte du facteur d'échelle réel d'une automatisation pour appréhender le fonctionnement global du système et son architecture, avec des approches plus formelles qui permettent de s'assurer que les propriétés intrinsèques des constituants contribuent efficacement au respect des exigences " système " formulées par les utilisateurs. <br />Le travail présenté dans ce mémoire définit donc une approche méthodologique basée sur le formalisme SysML (System Modeling Language) permettant l'identification, la formalisation et la structuration d'exigences globales relatives à un système, puis leur projection, sous forme de propriétés invariantes, sur une architecture de composants. La vérification des exigences de sécurité, repose alors, d'une part, sur un raffinement prouvé (par theroem proving) des exigences " système " permettant d'établir leur équivalence avec un ensemble de propriétés intrinsèques relatives à chacun des composants, et d'autre part, sur la vérification formelle (par model checking) de ces propriétés intrinsèques.

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>Today’s electronics in aviation (avionics) are more complex than ever before. With higher requirements on safety and reliability and with new SoC (System on Chip) technology, the validation and verification of designs meet new challenges. In commercial and military aircraft there are many safety-critical systems that need to be reliable. The consequences of a failure of a safety-critical system onboard a civil or military aircraft are immeasurably more serious than a glitch or a bit-flip in a consumer appliance or Internet service delivery. If possible hazards are found early in the design process, a lot of work can be saved later on. Certain structures in the code are prone to produce glitchy logic and timing problems and should be avoided. This thesis will strengthen Saab Avitronics knowledge of adaptable rule checking tools for HDL, with a market analysis of the tools available. Moreover will it evaluate two of the most suitable tools and finally it will describe some of the design issues that exist when coding safety-critical systems. Finally it is concluded that the introduction of static rule checking tools will help the validator to find dangerous constructs in the code. However, it will not be possible to fully automate rule checking for safety-critical systems, because of the high requirements on reliability.</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>

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.