Relevant bibliographies by topics / Systèmes, Conception de – Méthodes formelles (informatique) / Dissertations / Theses
To see the other types of publications on this topic, follow the link: Systèmes, Conception de – Méthodes formelles (informatique).

Dissertations / Theses on the topic 'Systèmes, Conception de – Méthodes formelles (informatique)'

Author: Grafiati
Published: 31 May 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the top 50 dissertations / theses for your research on the topic 'Systèmes, Conception de – Méthodes formelles (informatique).'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.

1

Berner, David. "Utilisation de méthodes formelles dans la conception conjointe de systèmes embarqués." Rennes 1, 2006. http://www.theses.fr/2006REN1S015.

Full text
Abstract:
La modélisation du contenu des puces pour systèmes embarqués s'avère de plus en plus difficile puisque le développement des outils et des méthodologies de modélisation n'a pas su accompagner l'explosion de la complexité des systèmes. Les méthodes formelles ont su démontrer dans les dernières années leurs capacités de prévention et de détection d'erreurs, ainsi que leurs avantages dans l'expression univoque de demandes et dans la spécification de systèmes. Malgré cela, leur utilisation reste toujours restreinte en raison d'un manque de liens avec les méthodes existantes et la difficulté de leur
APA, Harvard, Vancouver, ISO, and other styles
2

Prigent, Armelle. "Le test des systèmes temps-réel paramétrés : application à la conception d'architectures avioniques." Nantes, 2003. http://www.theses.fr/2003NANT2097.

Full text
Abstract:
Les systèmes embarqués critiques doivent être soumis à une validation rigoureuse afin d'assurer leurs performances et leur sûreté de fonctionnement. Le test de conformité est l'activité permettant de s'assurer que le produit final correspond aux attentes de la spécification. Dans le cas des systèmes temps-réel, il est important de tester la conformité en prenant en considération les contraintes temporelles du modèle. Cette thèse propose une approche de génération de tests pour des systèmes d'automates temporisés paramétrés. L'algorithme de construction des tests utilise un objectif de test pou
APA, Harvard, Vancouver, ISO, and other styles
3

Syed, Alwi Syed Hussein. "Vérification compositionnelle pour la conception sûre de systèmes embarqués." Paris 6, 2013. http://www.theses.fr/2013PA066230.

Full text
Abstract:
Afin d’améliorer la vérification de systèmes synchrones synthétisables, une méthode de vérification par model-checking basée sur une procédure de raffinement d’abstraction s’appuyant sur la structure en composants du système est proposée. Ayant opté pour la génération d'abstraction à partir des propriétés vérifiées des composants, différentes méthodes de sélection de propriétés pour l'abstraction initiale et les stratégies de raffinement pour améliorer le modèle abstrait sont présentées et analysées. La stratégie la plus directe est la technique de la Négation du Contre-exemple qui raffine le
APA, Harvard, Vancouver, ISO, and other styles
4

Kehren, Christophe. "Motifs formels d'architectures de systèmes pour la sûreté de fonctionnement." Phd thesis, Ecole nationale superieure de l'aeronautique et de l'espace, 2005. http://tel.archives-ouvertes.fr/tel-00011496.

Full text
Abstract:
Cette thèse propose des méthodes assistant la modélisation et l'évaluation qualitative de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces architectures sont souvent construites à partir de motifs généraux d'architectures de systèmes correspondant à des mécanismes de sûreté récurrents comme des redondances, des détections, etc. En s'inspirant des principes des "patrons de conception" développés en génie logiciel, nous avons proposé une modélisation de ces mécanismes et des attributs permettant leur réutilisation lors des analyses de sûreté de fonctionnement. Ces
APA, Harvard, Vancouver, ISO, and other styles
5

Lamboley, Patrick. "Proposition d'une méthode formelle d'automatisation de systèmes de production à l'aide de la méthode B." Nancy 1, 2001. http://www.theses.fr/2001NAN10177.

Full text
Abstract:
Les travaux s'inscrivent dans le cadre d'une ingénierie système afin de faciliter, au plus tôt, une représentation commune et consensuelle des services attendus d'un système automatisé par les différents acteurs du procédé d'automatisation. Ils ont pour objet de proposer, notamment dans la phase initiale de spécification, une méthode formelle vérifiant le prédicat d'automatisation : Spécifications des processus de commande ^ Spécifications des processus opérants => Spécifications des objectifs "système". De manière complémentaires aux travaux développés en Automatique, dans le cadre de la t
APA, Harvard, Vancouver, ISO, and other styles
6

Hamon, Juan Carlos. "Méthodes et outils de la conception amont pour les systèmes et les microsystèmes." Toulouse, INPT, 2005. http://ethesis.inp-toulouse.fr/archive/00000111/.

Full text
Abstract:
Ce travail de thèse porte sur l'élaboration de modèles de haut-niveau de systèmes pluridisciplinaires à base d'électronique. L'objectif est de réaliser des prototypes virtuels de ces systèmes et de vérifier formellement leur comportement dès les premières étapes du cycle de conception. Grâce à une approche descendante et au formalisme HiLeS, nous réalisons des représentations hiérarchiques qui associent des réseaux de Petri à un ensemble de blocs et de canaux interagissant mutuellement. Nous avons développé l'outil HiLeS Desiner pour rendre utilisable le formalisme avec plusieurs améliorations
APA, Harvard, Vancouver, ISO, and other styles
7

Sarray, Ines. "Conception de systèmes de reconnaissance d’activités humaines." Thesis, Université Côte d'Azur (ComUE), 2019. http://www.theses.fr/2019AZUR4016.

Full text
Abstract:
La reconnaissance d'activités est un domaine de recherche qui vise à décrire, analyser, reconnaître, comprendre et suivre les activités et les mouvements de personnes, d'animaux, ou d'objets animés. De nombreux domaines d'applications, importants et critiques, tels que la surveillance, la sécurité ou la santé, nécessitent une certaine forme de reconnaissance d'activités (humaines). Dans ces domaines, la reconnaissance d'activités peut être utile pour détecter tôt les comportements anormaux de certaines personnes : actes de vandalisme ou difficultés dues à l'âge ou la maladie. Les systèmes de r
APA, Harvard, Vancouver, ISO, and other styles
8

Lohr, Christophe. "Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-Lotos." Phd thesis, Institut National Polytechnique de Toulouse - INPT, 2002. http://tel.archives-ouvertes.fr/tel-00005228.

Full text
Abstract:
Ce mémoire de thèse s'intéresse à la conception de systèmes temps-réel en s'appuyant sur la méthode formelle RT-Lotos, extension temporelle à l'algèbre de processus Lotos. Il aborde plusieurs points relatifs à la spécification, la validation et l'ordonnancement de systèmes concurrents sujets à des contraintes logiques et temporelles. La première partie propose un éventail de méthodes formelles pour la spécification et la validation de systèmes temps-réel. Elle présente également le langage RT-Lotos et la technique de vérification formelle associée basée sur une analyse d'accessibilité. Elle dé
APA, Harvard, Vancouver, ISO, and other styles
9

Aljer, Ammar. "Co-design et raffinement en B : BHDL tool, plateforme pourr la conception de composants numériques." Lille 1, 2004. https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/2004/50376-2004-Aljer.pdf.

Full text
Abstract:
Dans le cadre de la modélisation de systèmes complexes, la conception d'entrée ou appelée système représente le plus haut niveau d'abstraction du système global, ceci avant tout choix en terme d'implantation et de technologies. À ce tout premier stade de la conception, l'utilisation d'un langage formel de spécification est de plus en plus considéré comme le fondement d'un réel processus de validation en particulier dans le cas d'exigences de sûreté. Cette thèse met en lumière la nécessité d'une modélisation par raffinement: de la spécfication la plus abstraite vers un point de description proc
APA, Harvard, Vancouver, ISO, and other styles
10

Filipiak, Alicia. "Conception et analyse formelle de protocoles de sécurité, une application au vote électronique et au paiement mobile." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0039/document.

Full text
Abstract:
Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos cont
APA, Harvard, Vancouver, ISO, and other styles
11

Arcile, Johan. "Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs : application aux véhicules autonomes communicants." Thesis, Université Paris-Saclay (ComUE), 2019. http://www.theses.fr/2019SACLE029.

Full text
Abstract:
Cette thèse est motivée par la question de la validation de propriétés dans un système composé de plusieurs agents mobiles prenants individuellement des décisions en temps réel.Chaque agent a une perception de l'environnement qui lui est propre et peut communiquer avec les autres agents à proximité.L'application qui a été choisie comme cas d'étude est celle des véhicules autonomes, qui du fait du large nombre de variables impliquées dans la représentation de tels systèmes, rend impossible des approches naïves.Les problématiques traitées concernent, d'une part, la modélisation d'un tel système,
APA, Harvard, Vancouver, ISO, and other styles
12

Bernard, Romain. "Analyses de sûreté de fonctionnement multi-systèmes." Phd thesis, Université Sciences et Technologies - Bordeaux I, 2009. http://tel.archives-ouvertes.fr/tel-00441310.

Full text
Abstract:
Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l'aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l'outil de model-checking
APA, Harvard, Vancouver, ISO, and other styles
13

Sampaio, Paulo Nazarena Maia. "Conception formelle de documents multimédia interactifs : une approche s'appuyant sur RT-Lotos." Toulouse 3, 2003. http://www.theses.fr/2003TOU30020.

Full text
Abstract:
Cette thèse présente une méthodologie pour la conception formelle de documents multimédia interactifs s'appuyant sur la technique de description formelle RT-LOTOS. La complexité de ces documents et l'utilisation de modèles auteur de haut niveau pour leur édition peuvent amener l'auteur, dans certains cas, à spécifier des relations de synchronisation qui ne pourront pas être satisfaites lors de la présentation du document, caractérisant ainsi des situations d'incohérence temporelle. D'où le besoin d'utiliser, lors de la conception d'un document, des techniques permettant de donner une sémantiqu
APA, Harvard, Vancouver, ISO, and other styles
14

Mokrani, Hocine. "Assistance au raffinement dans la conception des systèmes embarqués." Thesis, Paris, ENST, 2014. http://www.theses.fr/2014ENST0029/document.

Full text
Abstract:
La dernière décennie, la complexité des technologies embarqués a explosé et les flots de conception industrielle habituels ne suffisent plus pour proposer des produits fiables en respectant les exigences du marché. Ainsi, le développement de nouvelles méthodologies de conception est devenu un besoin impératif. La thèse vise l'amélioration des méthodologies de conception des systèmes embarqués. En proposant une approche de conception par niveaux d’abstraction, la nouvelle approche permet de guider et d’assister les concepteurs dans les étapes de conception, précisément de raffiner les composant
APA, Harvard, Vancouver, ISO, and other styles
15

Kherroubi, Souad. "Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0230/document.

Full text
Abstract:
Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. No
APA, Harvard, Vancouver, ISO, and other styles
16

Sagaspe, Laurent. "Allocation sûre dans les systèmes aéronautiques : Modélisation, Vérification et Génération". Phd thesis, Université Sciences et Technologies - Bordeaux I, 2008. http://tel.archives-ouvertes.fr/tel-00906924.

Full text
Abstract:
Cette thèse propose un cadre afin de modéliser, vérifier et générer des allocations de fonctions d'un système embarqué sur des ressources avioniques. Ce cadre est fondé sur l'utilisation du langage Altarica pour décrire formellement la propagation des défaillances au sein d'un système embarqué, sur l'utilisation de techniques de vérification tel que le "model-checking" et la génération d'arbre de défaillances et sur les techniques de résolution de contraintes. Les travaux sont illustrés par deux études de cas: l'allocation de ressources de calcul et de communication à une fonction de "suivi de
APA, Harvard, Vancouver, ISO, and other styles
17

El, Jamal Mohamad Hani. "Contribution à l'évolution des exigences et son impact sur la sécurité." Phd thesis, Université Paul Sabatier - Toulouse III, 2006. http://tel.archives-ouvertes.fr/tel-00139543.

Full text
Abstract:
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.
APA, Harvard, Vancouver, ISO, and other styles
18

Mohand, Oussaïd Linda. "Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie." Thesis, Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique, 2014. http://www.theses.fr/2014ESMA0022/document.

Full text
Abstract:
Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multimodales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multimodales en sortie. Le modèle p
APA, Harvard, Vancouver, ISO, and other styles
19

Methni, Amira. "Méthode de conception de logiciel système critique couplée à une démarche de vérification formelle." Thesis, Paris, CNAM, 2016. http://www.theses.fr/2016CNAM1057/document.

Full text
Abstract:
Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficult
APA, Harvard, Vancouver, ISO, and other styles
20

Fournier, Émilien. "Accélération matérielle de la vérification de sûreté et vivacité sur des architectures reconfigurables." Electronic Thesis or Diss., Brest, École nationale supérieure de techniques avancées Bretagne, 2022. http://www.theses.fr/2022ENTA0006.

Full text
Abstract:
Le Model-Checking est une technique automatisée, utilisée dans l’industrie pour la vérification, enjeu majeur pour la conception de systèmes fiables, cadre dans lequel performance et scalabilité sont critiques. La vérification swarm améliore la scalabilité par une approche partielle reposant sur l’exécution concurrente d’analyses randomisées. Les architectures reconfigurables promettent des gains de performance significatifs. Cependant, les travaux existant souffrent d’une conception monolithique qui freine l’exploration des opportunités des architectures reconfigurable. De plus, ces travaux s
APA, Harvard, Vancouver, ISO, and other styles
21

Pham, Thi-Kim-Dung. "Development of Correct-by-Construction Software using Product Lines." Thesis, Paris, CNAM, 2017. http://www.theses.fr/2017CNAM1138/document.

Full text
Abstract:
Nous avons commencé la thèse par la littérature d'enquête sur les approches SPLE et CbyC dans l'état de l'art. Sur la base de l'aperçu et des connaissances obtenues, nous avons analysé les problèmes existants et suggéré des moyens de les résoudre pour notre objectif principal. Nous avons proposé dans le chapitre 2 une méthodologie pour développer des lignes de produits afin que les produits générés soient corrects par construction. Notre intention principale est qu'un utilisateur n'a pas besoin de connaître le processus de génération de produit mais peut recevoir un produit final correct en sé
APA, Harvard, Vancouver, ISO, and other styles
22

Courtault, Jean-René. "Logiques de ressources dynamiques : modèles, propriétés et preuves." Thesis, Université de Lorraine, 2015. http://www.theses.fr/2015LORR0033/document.

Full text
Abstract:
En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous défin
APA, Harvard, Vancouver, ISO, and other styles
23

Garnier, Ilias. "Formalisme pour la conception haut-niveau et détaillée de systèmes de contrôle-commande critiques." Phd thesis, Université Paris Sud - Paris XI, 2012. http://tel.archives-ouvertes.fr/tel-00676901.

Full text
Abstract:
L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'inf
APA, Harvard, Vancouver, ISO, and other styles
24

Nastov, Blazo. "Contribution à une méthode outillée pour la conception de langages de modélisation métier interopérables, analysables et prouvables pour l'Ingénierie Système basée sur des Modèles." Thesis, Montpellier, 2016. http://www.theses.fr/2016MONTT272/document.

Full text
Abstract:
L'Ingénierie des Systèmes (IS) est une approche pluridisciplinaire et collaborative pour mener à bâtir et structurer la conception puis la réalisation et le développement de systèmes complexes. L’IS repose à la fois sur une approche processus et sur la mise en oeuvre de modèles de systèmes s'appuyant de fait dans un contexte basé ou dirigé par des modèles. On parle alors d’Ingénierie Système Basée sur des Modèles (ISBM ou Model based Systems Engineering MBSE). L’ISBM introduit des concepts, méthodes et techniques pour construire et gérer des modèles. Elle a pour objectif l’atteinte et l’amélio
APA, Harvard, Vancouver, ISO, and other styles
25

Petit, Mathieu. "Approche spatiale pour la caractérisation du contexte d'exécution d'un système d'information ubiquitaire." Phd thesis, Paris, ENSAM, 2010. http://pastel.archives-ouvertes.fr/pastel-00511919.

Full text
Abstract:
Les nouvelles technologies en matière d'accès à l'information, de communication sans-fil et de localisation d'informations ouvrent la voie à des innovations majeures dans l'utilisation des systèmes informatiques. Ces avancées permettent d'imaginer de nouveaux usages informatiques dont la mise en œuvre motive le développement de méthodes de conception appropriées. Plus particulièrement, l'informatique mobile combine désormais des enjeux conceptuels tels que l'accès à des services par un utilisateur en mobilité, la généralisation d'outils de localisation, la compréhension de systèmes complexes p
APA, Harvard, Vancouver, ISO, and other styles
26

Yang, Faqing. "Un environnement de simulation pour la validation de spécifications B événementiel." Phd thesis, Université de Lorraine, 2013. http://tel.archives-ouvertes.fr/tel-00951922.

Full text
Abstract:
Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour
APA, Harvard, Vancouver, ISO, and other styles
27

Pagani, Florence. "Ordres partiels pour la vérification de systèmes temps réel." Toulouse, ENSAE, 1997. http://www.theses.fr/1997ESAE0005.

Full text
Abstract:
Si l'utilité des méthodes de vérification formelle des systèmes temps réel est désormais reconnue, leur application à des systèmes complexes est encore freinée par les performances des outils disponibles. En particulier, la vérification de modèles fondée sur l'exploration exhaustive de l'espace des états d'un système est souvent limitée par ce que l'on appelle l'explosion combinatoire des états. Ce phénomène est encore accentué lorque des aspects quantitatifs (durée des actions par exemple) sont introduits dans le modèle. Une partie de l'xplosion combinatoire est due à la modélisation du paral
APA, Harvard, Vancouver, ISO, and other styles
28

Wiels, Virginie. "Modularité pour la conception et la validation formelles de systèmes." Toulouse, ENSAE, 1997. http://www.theses.fr/1997ESAE0001.

Full text
Abstract:
Structuration et compositionnalité sont des besoins importants dans le domaine des techniques formelles pour maîtriser la taille et la complexité des spécifications. Nous proposons un formalisme qui permet de spécifier des systèmes de façon modulaire, mais aussi d'exploiter la structure des spécifications pour réaliser des vérifications modulaires. Un outil de spécification (Moka) est associé à ce formalisme et peut être combiné avec des outils de démonstration logique existants. L'approche est illustrée sur trois applications de domaines différents. Nous mettons d'abord l'accent sur les besoi
APA, Harvard, Vancouver, ISO, and other styles
29

Radhouani, Amira. "Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information." Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM025/document.

Full text
Abstract:
La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilis
APA, Harvard, Vancouver, ISO, and other styles
30

Fayolle, Thomas. "Combinaison de méthodes formelles pour la spécification de systèmes industriels." Thesis, Paris Est, 2017. http://www.theses.fr/2017PESC1078/document.

Full text
Abstract:
La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Even
APA, Harvard, Vancouver, ISO, and other styles
31

Proch, Cyril. "Assistance au développement incrémental et prouvé de systèmes enfouis." Nancy 1, 2006. http://docnum.univ-lorraine.fr/public/SCD_T_2006_0012_PROCH.pdf.

Full text
Abstract:
Les méthodes de développement rigoureuses ne se sont pas encore imposées en électronique. La validation des systèmes se fait par des séries de tests ou par l'utilisation de model checker ne couvrant pas toutes les possibilités. Nous avons élaboré une méthode de développement par la preuve en nous appuyant sur une étude de cas (TV numérique). Le raffinement est central à nos travaux car il permet de conserver la traçabilité et distribue la complexité du système et des preuves. Les modèles construits aident aux choix architecturaux en structurant les tâches du système. Nous avons proposé un méca
APA, Harvard, Vancouver, ISO, and other styles
32

Imine, Abdessamad. "Conception Formelle d'Algorithmes de Réplication Optimiste Vers l'Edition Collaborative dans les Réseaux Pair-à-Pair." Nancy 1, 2006. http://www.theses.fr/2006NAN10184.

Full text
Abstract:
Les systèmes d'édition collaborative permettent la manipulation d'objets, comme des documents texte, par plusieurs personnes qui sont réparties dan le temps et dans l'espace. La réplication des objets est indispensable dans de tels systèmes mais elle peut entraîner un problème de divergence de données. Pour pallier ce problème, une approche optimiste, appelée transformation opérationnelle, est utilisée dans ce domaine. L'objectif de cette thèse est de proposer un cadre formel pour la conception d'algorithmes de transformation corrects qui peuvent être déployés sur des systèmes d'édition collab
APA, Harvard, Vancouver, ISO, and other styles
33

Sagaspe, Laurent. "Allocation sûre dans les systèmes aéronautiques : modélisation, vérification et génération." Thesis, Bordeaux 1, 2008. http://www.theses.fr/2008BOR13707/document.

Full text
Abstract:
Les architectures des systèmes embarqués des nouvelles générations d'avions civils et militaires tendent à s'organiser autour d'une plateforme avionique constituée de calculateurs interconnectés par un réseau central. Ce type d'architecture a fait apparaitre le besoin de développer de nouvelles méthodes de conception afin d'assister le dialogue entre les concepteurs des fonctions à embarquer (commandes de vol, gestion de l'énergie, ...) et les architectes de la plateforme avionique. Il est, en particulier, primordial de s'assurer que l'allocation des ressources de la plateforme aux fonctions e
APA, Harvard, Vancouver, ISO, and other styles
34

Doche, Marielle. "Techniques formelles pour l'évaluation de systèmes critiques complexes : test et modularité." École nationale supérieure de l'aéronautique et de l'espace (Toulouse ; 1972-2007), 1999. http://www.theses.fr/1999ESAE0024.

Full text
Abstract:
L'intérêt des méthodes formelles est de permettre le développement rigoureux de systèmes informatiques critiques. Pour des systèmes complexes, elles peuvent être complétées par des formalismes de structuration et de modularité. Nous proposons ici une démarche pour la génération et l'évaluation de jeux de test fonctionnel à partir de spécifications formelles structurées ou modulaires. Nous nous appuyons sur un formalisme de spécification modulaire Moka-TRIO basé d'une part sur la théorie des catégories et le calcul des modèles défini par Ehrig et Mahr (qui permettent de structurer une modélisat
APA, Harvard, Vancouver, ISO, and other styles
35

Hunel, Philippe. "Conception et réalisation d'un environnement intégré de génie logiciel pour le développement des protocoles." Clermont-Ferrand 2, 1994. http://www.theses.fr/1994CLF21624.

Full text
Abstract:
Le travail présenté dans cette thèse porte sur l'élaboration d'un environnement pour concevoir, spécifier et implanter des protocoles de communication en utilisant la Technique de Description Formelle (TDF) Estelle. Les différents outils courants d'aide au développement, basés sur Estelle, ne couvrent généralement pas l'ensemble des objectifs des différentes phases d'un développement de protocole. En outre, ils présentent souvent des interfaces utilisateur variés. Cette thèse propose une solution pour intégrer les outils Estelle existants ou à venir dans un environnement ouvert. La première pa
APA, Harvard, Vancouver, ISO, and other styles
36

Rauzy, Pablo. "Méthodes logicielles formelles pour la sécurité des implémentations de systèmes cryptographiques." Thesis, Paris, ENST, 2015. http://www.theses.fr/2015ENST0039/document.

Full text
Abstract:
Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités
APA, Harvard, Vancouver, ISO, and other styles
37

Sassolas, Mathieu. "Méthodes qualitatives et quantitatives pour la détection d'information cachée." Paris 6, 2011. http://www.theses.fr/2011PA066581.

Full text
Abstract:
Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système d
APA, Harvard, Vancouver, ISO, and other styles
38

Demangeon, Romain. "Terminaison des systèmes concurrents." Lyon, Ecole normale supérieure, 2010. http://www.theses.fr/2010ENSL0595.

Full text
Abstract:
Cette thèse propose une étude de la terminaison dans les systèmes concurrents. La terminaison est une propriété désirable pour les programmes en elle même et comme prérequis pour d'autres propriétés. La cadre du pi calccul est présente dans la section 2. Dans la section 3, des systèmes de types de bases sur le poids sont présentés. Dans la section 4, on montre comment utiliser des approches pour aborder la question de la terminaison des langages concurrents d'ordre supérieur. Dans la section 5, on propose une étude de la complexité du problème de l'inférence pour les analyses basées sur le poi
APA, Harvard, Vancouver, ISO, and other styles
39

Chauvel, Franck. "Méthodes et outils pour la conception de systèmes logiciels auto-adaptatifs." Phd thesis, Université de Bretagne Sud, 2008. http://tel.archives-ouvertes.fr/tel-00512189.

Full text
Abstract:
Because of the increasing need of mobiles devices, most of software systems need to take into account a highly dynamic environment including hardware and software resources. This need for self-adaptation arises in both large-scale systems such as peer-to-peer systems and small-scale systems such as embedded systems. Those systems, so called ``self-adaptive systems'', have to observe the changes which occur in their environment in order to maximize the quality of the services they provide. ``Observation, Decision, Action'' have thus become the three basic capabilities of self-adaptive systems.
APA, Harvard, Vancouver, ISO, and other styles
40

Masson, Lola. "Safety monitoring for autonomous systems : interactive elicitation of safety rules." Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30220.

Full text
Abstract:
Un moniteur de sécurité actif est un mécanisme indépendant qui est responsable de maintenir le système dans un état sûr, en cas de situation dangereuse. Il dispose d'observations (capteurs) et d'interventions (actionneurs). Des règles de sécurité sont synthétisées, à partir des résultats d'une analyse de risques, grâce à l'outil SMOF (Safety MOnitoring Framework), afin d'identifier quelles interventions appliquer quand une observation atteint une valeur dangereuse. Les règles de sécurité respectent une propriété de sécurité (le système reste das un état sûr) ainsi que des propriétés de permiss
APA, Harvard, Vancouver, ISO, and other styles
41

Bonnefoi, Fabien. "Vérification formelle des spécifications de systèmes complexes par réseaux de Petri : application aux systèmes de transport intelligents." Paris 6, 2010. http://www.theses.fr/2010PA066616.

Full text
APA, Harvard, Vancouver, ISO, and other styles
42

Tchuenkam, Tchoneng Honoré. "Techniques formelles pour le développement de systèmes de conduite de procédés manufacturiers : abstraction, spécification, synthèse et optimisation." Nancy 1, 1991. http://www.theses.fr/1991NAN10413.

Full text
Abstract:
Nous utilisons des techniques classiques d'abstraction, de spécification et de synthèse de programmes pour proposer une démarche de développement formel de systèmes temps réels dans le cadre (restreint) de la conduite des processus de productions discrètes. Dans le type de problème que nous avons à traiter, on dispose d'une installation industrielle dont les composants assurent des fonctions élémentaires de transformation, d'assemblage et de manutention de produits. Ces composants peuvent être mis en marche par des actionneurs et des capteurs fournissent des renseignements sur l'état du systèm
APA, Harvard, Vancouver, ISO, and other styles
43

Darlot, Christophe. "Reformulation et vérification de propriétés temporelles dans le cadre du raffinement de systèmes d'évènements." Besançon, 2002. http://www.theses.fr/2002BESA2054.

Full text
Abstract:
Les travaux présentés se placent dans le contexte de la vérification de propriétés temporelles sur des systèmes d'événements spécifiés par raffinement. Notre démarche se décompose en quatre étapes : 1-Nous vérifions une propriété abstraite par model-checking; 2- Nous raffinons le système et vérifions ce raffinement ; 3- Nous raffinons la propriété abstraite en une propriété dite reformulée; 4- Nous vérifions la propriété reformulée. L'apport de ces travaux est d'une part de permettre à l'utilisateur de raffiner les propriétés pour tenir compte des détails introduits lors du raffinement, d'autr
APA, Harvard, Vancouver, ISO, and other styles
44

Gervais, Frédéric. "Combinaison de spécifications formelles pour la modélisation des systèmes d'information." Phd thesis, Conservatoire national des arts et metiers - CNAM, 2006. http://tel.archives-ouvertes.fr/tel-00121006.

Full text
Abstract:
L'objectif de cette thèse est de profiter des avantages de deux formes de modélisation complémentaires pour représenter de manière formelle les systèmes d'information (SI). Un SI est un système informatisé qui permet de rassembler les informations d'une organisation et qui fournit des opérations pour les manipuler. Les SI considérés sont développés autour de systèmes de gestion de bases de données (SGBD). Notre motivation est d'utiliser des notations et des techniques formelles pour les concevoir, contrairement aux méthodes actuelles qui sont au mieux semi-formelles. D'une part, EB3 est un lan
APA, Harvard, Vancouver, ISO, and other styles
45

Hachicha, Rim. "Modélisation et analyse de la flexibilité dans les systèmes workflow." Paris, CNAM, 2007. http://www.theses.fr/2007CNAM0565.

Full text
Abstract:
Cette thèse est consacrée à la modélisation formelle et la gestion des systèmes workflows. Nous nous intéressons à apporter une solution à l'un des principaux problèmes des systèmes workflows est celui de la flexibilité : les modèles aussi bien que les systèmes actuels ne sont pas suffisamment flexibles et adaptables. Dans ce but, nous proposons un modèle de tâches et d'acteurs précisant les relations formelles entre les tâches workflow et les acteurs et permettant une assignation flexible des acteurs ux activités workflow. L'allocation des tâches workflows est fondée sur le concept de distanc
APA, Harvard, Vancouver, ISO, and other styles
46

Belguidoum, Meriem. "Conception d'une infrastructure pour un déploiement sûr et flexible des composants logiciels." Télécom Bretagne, 2008. http://www.theses.fr/2008TELB0060.

Full text
Abstract:
Le déploiement de logiciels est une tâche complexe car elle nécessite la réalisation de nombreuses actions ayant de fortes contraintes de dépendance. Il recouvre toutes les activités qui composent le cycle de vie du logiciel depuis son développement jusqu’à son utilisation. Dans le cadre de ce travail, nous nous intéressons aux activités d’installation, de désinstallation et de mise à jour. En parallèle, les applications deviennent de plus en plus complexes, ce qui provoque une explosion de leur taille. Pour faciliter leur gestion et leur réutilisation, elles sont représentées par des collecti
APA, Harvard, Vancouver, ISO, and other styles
47

Mammar, Amel. "Un environnement formel pour le développement d'applications bases de données." Paris, CNAM, 2002. http://www.theses.fr/2002CNAM0437.

Full text
Abstract:
Ce travail présente une approche formelle pour le développement d'applications bases de données sûres. Cette approche consiste en la génération d'une implémentation relationnelle à partir de spécifications formelles. On décrit préalablement l'application à l'aide de notations UML, puis un processus automatique est appliqué afin de les traduire en spécifications B. En utilisant le processus de raffinement, un ensemble de règles de raffinement; opérant sur les données et les opérations, est utilisé sur les spécifications obtenues. Ces phases de raffinement ont pour but de rendre les spécificatio
APA, Harvard, Vancouver, ISO, and other styles
48

Colange, Maximilien. "Symmetry reduction and symbolic data structures for model-checking of distributed systems." Paris 6, 2013. http://www.theses.fr/2013PA066724.

Full text
Abstract:
Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparticroît exponentiellement avec son nombre de composants. Nous retenons deux des
APA, Harvard, Vancouver, ISO, and other styles
49

Jaeger, Éric. "Study of the benefits of using deductive formal methods for secure developments." Paris 6, 2010. http://www.theses.fr/2010PA066048.

Full text
Abstract:
La mise en oeuvre des méthodes formelles déductives lors du développement de systèmes permet d'obtenir des garanties mathématiques quant à leur validité. Pour cette raison, leur utilisation est recommandée ou exigée par certains standards relatifs à la sûreté de fonctionnement ou la sécurité. Il reste cependant légitime de s'interroger sur la portée exacte des bénéfices. Certains aspects d'un système peuvent échapper à la formalisation, et il n'est pas toujours facile d'identifier ces limitations ou leurs conséquences. De même, si la validité d'une preuve est difficilement contestable, son uti
APA, Harvard, Vancouver, ISO, and other styles
50

Collé, Frédéric. "Un modèle de conception centré interaction : formalisation et application à la conception de systèmes complexes." La Rochelle, 2006. http://www.theses.fr/2006LAROS168.

Full text
Abstract:
Nous nous intéressons à représenter, analyser et mettre en oeuvre le comportement dans des systèmes complexes (tels que des environnements de réalité augmentée), mobiles et évolutifs. Le travail effectué se situe dans une approche globale d’un outil d’aide à la conception de systèmes interactifs, i. E. Des systèmes s’appuyant sur une interaction forte avec un composant de visualisation. Pour ce faire, une approche de modélisation et de conception orientée agent est retenue. Plus particulièrement, nos travaux nous ont conduit à nous intéresser au développement d’un modèle et d’une méthode de co
APA, Harvard, Vancouver, ISO, and other styles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography