Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.

Au-delà de la formidable évolution en termes de complexité du circuit électronique en soi, son adoption et sa diffusion ont connu, au fil des dernières années, une explosion dans un très grand nombre de domaines distincts. Un système sur puce peut incorporer une combinaison de composants aux fonctionnalités très différentes. S'assurer du bon fonctionnement de chaque composant, et du système complet, est une tâche primordiale et épineuse. Dans ce contexte, l'Assertion-Based Verification (ABV) a considérablement gagné en popularité ces dernières années : il s'agit d'une démarche de vérification où des propriétés logico-temporelles, exprimées dans des langages tels que PSL ou SVA, spécifient le comportement attendu du design. Alors que la plupart des solutions d'ABV existantes se limitent au niveau transfert de registres (RTL), la contribution décrite dans cette thèse s'efforce de résoudre un certain nombre de limitations et vise ainsi une solution mature pour le niveau transactionnel (TLM) de SystemC. Une technique efficace de construction de moniteurs de surveillance à partir de propriétés PSL est proposée : cette technique, inspirée d'une approche originale existante pour le niveau RTL, est ici adaptée à SystemC TLM. Une méthode spécifique de surveillance des actions de communication à haut niveau d'abstraction est également détaillée. Les possibilités offertes par la technique présentée sont significativement étendues en proposant, pour les propriétés écrites en langage PSL, à la fois un support formel et une mise en oeuvre pratique pour des variables auxiliaires globales et locales, qui constituent un élément essentiel lors des spécifications à haut niveau d'abstraction. Tous ces concepts sont également implémentés dans un outil prototype. Afin d'illustrer l'intérêt de la solution proposée, diverses expérimentations sont effectuées avec des designs aux dimensions et complexités différentes. Les résultats obtenus permettent de souligner le fait que la méthode de vérification dynamique suggérée reste applicable pour des designs de taille réaliste.

Nous présentons un ensemble de travaux sur l'intégration de méthodes formelles et l'analyse multifacette de systèmes logiciels. %deuxième partie Partant de l'idée que les différentes facettes d'un système doivent être étudiées et développées avec les formalismes et outils appropriés, nous avons exploré, suite à d'autres chercheurs, des pistes pour l'intégration de méthodes formelles utilisées pour spécifier, analyser ou développer des parties des systèmes. La nécessité de l'intégration est relative au besoin de l'interaction entre différentes parties d'un même système ou bien à l'appréhension globale des propriétés du système. Nous explicitons les principaux problèmes de l'intégration de méthodes formelles : l'hétérogénéité syntaxique, l'hétérogénétité sémantique et la variété des systèmes logiques de raisonnement. Nous proposons alors la notion de compatibilité relative à ces trois niveaux pour assurer l'intégration de méthodes. L'idée principale est celle de l'interopérabilité sur une base sémantique (base d'intégration) ) sans laquelle aucun raisonnement n'est possible entre des parties assemblées d'un système. Les raisonnements formels sont alors effectués par plongement (embedding) des spécifications dans des logiques appropriées. Ce premier cadre est généralisé à des domaines de compatibilité plus larges que les bases d'intégration, et qui permettent de s'affranchir des langages et de travailler au niveau des paradigmes sous-jacents aux langages ; on obtient ainsi un cadre pour une intégration générique. Nous avons montré comment les formalismes intégrés existants tels que LOTOS, CSP-B, Circus rentrent dans ce cadre et nous avons mis en oeuvre ces idées pour de nouvelles intégrations par exemple B et les réseaux de Pétri. Dans une autre partie des travaux, nous présentons des extensions proposées autour de la méthode B, notamment la composition parallèle asynchrone de systèmes abstraits B à la manière de la composition parallèle dans les algèbres de processus. Notre proposition permet de combiner dans un même projet de développement formel la démarche descendante de la méthode B par une approche ascendante. Nous présentons ensuite une méthode de construction systématique de spécifications B pour des systèmes multi-processus à architecture dynamique. Ces travaux généralisent les précédents sur la composition de systèmes abstraits en définissant un opérateur de fusion de sous-systèmes qui est plus général que les opérateurs de composition parallèle. Une partie des travaux est consacrée à l'analyse multifacette de système ; notre proposition consiste à assurer la compatibilité des analyses des différentes facettes en partant non pas de modèles indépendants mais de modèles spécifiques dérivés à partir d'un modèle de référence qui permet d'assurer la cohésion globale de l'analyse. Cette approche est poursuivie par des expérimentations sur la combinaison de prouveurs et d'évaluateurs de modèles (model-checkers). Nous avons exploré d'autres voies pour l'analyse multifacette : élaborer une algèbre de spécifications multiparadigmes, ou différents aspects, relatifs aux facettes envisagées, peuvent être introduits dans une même unité de spécification. Les unités de spécification sont ensuite composées à l'aide des opérateurs de l'algèbre. Le lien est fait entre cette approche et celle de l'intégration de méthodes par plongement dans des logiques formelles. Une plateforme expérimentale est développée conjointement à ces travaux et relie les deux approches : elle permettra à terme de traduire, moyennant la compatibilité sémantique, différents formalismes d'entrées dans des formalismes cibles en passant par un modèle de référence ou pivot qui lui même est une spécification multiparadigme.

Actuellement, les applications interactives sont utilisées dans de nombreux domaines (guichets automatiques, tours de contrôle...), par des publics très différents (enfants, experts, handicapés...) et par un nombre important d'utilisateurs (interfaces de téléphones portables...) ou au contraire très spécifiques (logiciels conçus spécifiquement pour une entreprise). Elles sont de ce fait très diverses. De par la multiplicité des paramètres à prendre en compte, la conception et le développement des applications interactives sont devenus très coûteux. Afin de réduire ces coûts, des recherches sont actuellement menées sur le processus de conception. Cette thèse s'inscrit dans ces travaux. L'un des axes étudiés pour réduire le coût de production des applications interactives est la détection des erreurs le plus en amont possible pendant le processus de conception. Nous proposons de faciliter la vérification et la validation de la dynamique des applications (plus spécifiquement dénommée dialogue) tout au long de la conception, en fonction des spécifications recueillies auprès des futurs utilisateurs, exprimés sous forme de modèles de tâches. Les modèles de dialogue et les modèles de tâches représentent deux points de vue différents et complémentaires pour une même application. Nous proposons une approche de vérification de cohérence entre ces deux modèles tout au long du cycle de vie de l'application. Pour cela, nous avons défini des règles de cohérence entre les modèles que nous vérifions formellement en utilisant une méta-modélisation des formalismes que nous avons choisis après évaluation de leur utilisation pour une conception centrée-utilisateur.

<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>

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (1) on doit pouvoir disposer d'éléments de preuve fiables, (2) les comportements attendus des composants doivent avoir été définis préalablement et (3) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite ''acceptable'' qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en oeuvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.

Cette thèse est consacrée au problème de la vérification automatique des protocoles cryptographiques d'un point de vue logique et calculatoire.<br />Dans une première partie, nous abordons la sécurité des protocoles dans le cadre logique (formel). Nous montrons comment spécifier différentes propriétés de sécurité des protocoles (secret, authentification, <br />résistance aux attaques par dictionnaire) au moyen d'un langage de processus et comment les analyser de manière automatique pour un nombre borné de sessions.<br />La seconde partie traite de la justification cryptographique des modèles logiques. Nous nous intéressons ici à la notion d'équivalence statique, appliquée en particulier au chiffrement et aux données vulnérables aux attaques par dictionnaire (par ex. des mots de passe). Dans ce cadre, nous montrons que sous certaines conditions simples, toute preuve logique d'équivalence statique implique d'indistinguibilité cryptographique des données modélisées.

La complexité temporelle, logique et sémantique des systèmes multimédias et hypermédias rend nécessaire l'utilisation de techniques formelles permettant de spécifier ces systèmes et de vérifier, en préalable à leur conception, leurs propriétés logiques et temporelles. Cette thèse introduit une nouvelle technique de modélisation de systèmes multimédias et hypermédias basée sur le formalisme des réseaux de Pétri étendus par le temps. Ce modèle appelé Réseaux de Petri à Flux Temporels (RdPFT) permet de spécifier l'indéterminisme temporel intrinsèque aux systèmes distribués multimédias en associant un intervalle temporel aux arcs sortant des places d'un réseau de Petri. Les RdPFT introduisent de plus une sémantique formelle de la synchronisation en environnement faiblement synchrone. Cette sémantique formelle, définie à l'aide de 9 types de règles de tir pouvant être sélectivement associées aux transitions d'un RdPFT, permet de maîtriser l'indéterminisme de synchronisation introduit par la variabilité temporelle des traitements. Ainsi, les RdPFT permettent de modéliser de façon complète, précise et aisée les contraintes de synchronisation des systèmes multimédias. Cette thèse considère également la classe des RdPFT construits à l'aide des opérateurs de l'algèbre temporelle de Allen. Cette classe, appelée Réseaux de Petri Structurés à Flux Temporels (RdPSFT), permet une vérification aisée des propriétés temporelles d'un système multimédia et offre de plus des bases formelles pour la représentation abstraite des structures logiques et temporelles d'un système multimédia. Finalement cette thèse introduit une extension des RdPFT, appelée Réseaux de Petri Hiérarchisés à Flux Temporels (RdPHFT). Cette extension, bénéficiant de tous les acquis théoriques des RdPFT, permet de modéliser à l'aide d'un formalisme unificateur les composants d'un système hypermédia et introduit une sémantique formelle de la notion de synchronisatio n hypermédia. De plus les RdPHFT offrent un support méthodologique permettant une spécification modulaire et hiérarchisée des systèmes hypermédias, et plus généralement des systèmes "à contraintes temporelles"

Cette thèse propose un modèle formel et une méthodologie, permettant la conception formelle de documents hypermédias portables, qui couvre toutes les étapes essentielles du cycle de développement des documents hypermédias. Nous avons défini un modèle formel permettant la spécification et l'analyse des documents. L'implémentation est supportée par la traduction de la spécification analysée en une représentation physique interprétable par un système de présentation. Nous avons aussi développé des outils mettant en oeuvre cette méthodologie. Le modèle formel proposé est une extension du modèle Réseaux de Pétri Hiérarchiques à Flux Temporel (RdPHFT), qui permet une spécification formelle unifiée et précise de la synchronisation logique et temporelle des systèmes hypermédias distribués. Le modèle RdPHFT n'a pas pour objectif la description complète de documents hypermédias. Cette thèse propose une version interprétée du modèle RdPHFT, appelée RdPHFT-I, qui étend le modèle RdPHFT afin de permettre la spécification complète de documents hypermédias. A la suite et à l'aide du modèle RdPHFT-I, nous proposons une méthodologie de prototypage de documents hypermédias dans laquelle la spécification et l'analyse des documents sont faites à l'aide du modèle RdPHFT-I et l'implantation est supportée : soit par la production automatique de représentations MHEG, soit par la production d'applications Java. MHEG est une norme internationale de représentation des informations multimédias et hypermédias permettant le transfert de ces informations dans un système ouvert. Java est un langage de programmation d'applications multimédias fournissant un code portable de l'application. En résumé, la principale contribution de ce travail est d'avoir proposé et mis en oeuvre une méthodologie permettant de contrôler la qualité et de maîtriser la complexité des systèmes hypermédias, à partir d'un cycle de vie permettant de générer directement un docume nt hypermédia à partir d'une spécification formelle analysée.

Le travail de la thèse porte sur la problématique de l'évolution des exigences et son analyse d'impact sur la sécurité. Au cours du développement des systèmes, les parties prenantes demandent l'application des évolutions, afin d'améliorer leurs fonctionnalités. L'occurrence d'une évolution affecte plusieurs aspects comme: la sécurité, le coût du développement et les délais. Lorsque le développement concerne un système complexe où le nombre des exigences est de l'ordre de dizaines de milliers, alors les demandes des évolutions rendent l'analyse d'impact du changement de plus en plus difficile. Malheureusement, la problématique de l'évolution des exigences n'est pas encore complètement résolue en milieu industriel. Notre étude est située dans le contexte d'ingénierie système et ingénierie des exigences, en intégrant des modèles formels et outils supports associés pour la vérification des propriétés de sécurité. La méthodologie est basée sur la norme industrielle de l'EIA-632 et sur le format VOLERE d'ingénierie des exigences en intégrant un modèle de traçabilité. De cette démarche ingénierie système, on a développé une méthodologie associée et un système d'information du processus de changement/évolution des exigences. Enfin, ce travail présente la méthodologie de la recherche d'impact lors de la demande de changement, et les outils qui supportent la méthodologie de la recherche d'impact, en se basant sur la méthode formelle (RAISE), qui nous permet d'analyser l'impact de l'évolution sur la sécurité.