Dissertations / Theses on the topic 'Spécification de protocoles'
To see the other types of publications on this topic, follow the link: Spécification de protocoles.
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 36 dissertations / theses for your research on the topic 'Spécification de protocoles.'
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
Duchene, Julien. "Développement et évaluation d'obfuscations de protocoles basées sur la spécification." Electronic Thesis or Diss., Toulouse, INSA, 2018. http://www.theses.fr/2018ISAT0054.
Full textAbstract:
Il existe de plus en plus de protocoles de communications différents. La spécification de beaucoup d’entre eux est disponible. Cependant, quand il s’agit de moyens de communication propriétaires, cette spécification est gardée secrète : un attaquant qui aurait accès à cette spécification pourrait compromettre un système utilisant ce protocole. Même s’il n’a pas accès à cette spécification, l’attaquant peut l’obtenir par rétro-conception. Ainsi, il est intéressant de créer des protocoles qui sont difficiles à rétro-concevoir. Dans cette thèse, nous proposons une nouvelle approche spécifiquement développée pour rendre complexe la rétro-conception de protocole. Nous appliquons pour cela des obfuscations au format du message et ceci de façon automatique à partir de la spécification du protocole. Pour cela, nous avons dans un premier temps étudié plus de 30 contributions différentes concernant des outils de rétro-conception de protocole et en avons tiré des conclusions suivantes : 1) les outils de rétro-conception de protocole pratiquent l’inférence de modèles réguliers ; 2) ils supposent que le parsing d’un message s’effectue de gauche à droite ; 3) ils délimitent le message en champs d’après des délimiteurs bien connus ou via des algorithmes ad-hoc ; 4) ils regroupent les messages d’après des mesures de similarité sur des patterns. Ainsi, pour créer un protocole difficile à rétro-concevoir, une solution est de s’assurer que le protocole ne respecte pas ces conditions. Dans un second temps, nous avons donc proposé un modèle de format de messages qui permet l’application d’obfuscations. Nous avons défini des obfuscations atomiques qui peuvent être composées. Chacune de ces obfuscations cible une ou plusieurs des hypothèses des outils de rétro-conception. La composition des obfuscations assure l’efficacité de notre solution et rend la rétro-conception de protocole complexe. Ce modèle est utilisé pour générer automatiquement le code du parseur, du sérialiseur et des accesseurs. Cette solution est implémentée dans un prototype nommé ProtoObf grâce auquel nous avons pu évalué les performances des obfuscations. Les résultats montrent une nette augmentation de la complexité de la rétro-conception avec le nombre de compositions d’obfuscation tandis que les coûts induits (particulièrement la taille du buffer sérialisé) restent basThere are more and more protocols. Many of them have their specification available for interoperability purpose for instance. However, when it comes to intellectual property, this specification is kept secret. Attackers might use a wrongly implemented protocol to compromise a system, if he has access to the specification, it’s attack would be far more efficient. Even if he does not have access to the specification, he can reverse-engine it. Thus, create protocols hard to reverse is interesting. In this thesis, we develop a novel approach of protocol protections to make protocol reverse engineering more complex. We apply some obfuscations on protocol message format, furthermore, we do it automatically from the original protocol specification. Firstly, we have analyzed more than 30 different contributions of protocol reverse engineering tools. We retrieved the following elements : 1) Protocol reverse engineering tools try to infer regular models ; 2) They suppose that the parsing is done from left to right ; 3) They delimit fields based on well-known delimiters or with ad-hoc techniques ; 4) They cluster messages based on pattern similarity measures. Thus, to make protocol reverse harder, one can create protocols which does not respect theses statements. Secondly, we have proposed a model of message format on which obfuscations can be applied. With this model, we also provide some atomic obfuscations which can be composed. Each obfuscation target one or more protocol reverse engineering hypothesis. Obfuscation composition ensures effectiveness of our solution and makes protocol reverse-engineering more complex. This model is used to automatically generate code for parser, serializer and accessors. This solution is implemented into a framework we called ProtoObf. ProtoObf is used to evaluate obfuscations performance. Results show an increase of protocol complexity with the number of obfuscation composition while costs (particularly the serialized buffer size) stay low
2
Chatzikokolakis, Konstantinos. "Spécification et vérification des protocoles de sécurité probabilistes." Phd thesis, Ecole Polytechnique X, 2007. http://pastel.archives-ouvertes.fr/pastel-00003950.
Full textAbstract:
Le concept de l'anonymat entre en jeu dans les cas où nous voulons garder le secret sur l'identité des agents qui participent à un certain événement. Il existe un large éventail de situations dans lesquelles cette propriété peut être nécessaire ou souhaitable, par exemple: web de vote surf, les dons anonymes, et l'affichage sur les babillards. L'anonymat est souvent formulées de manière plus générale comme une propriété de dissimulation d'informations, à savoir la propriété qu'une partie des informations relatives à un certain événement est tenu secret. Il faut être prudent, cependant, de ne pas confondre anonymat avec d'autres propriétés que la même description, notamment la confidentialité (secret aka). Laissez-nous insister sur la différence entre les deux concepts en ce qui concerne l'envoi de messages: la confidentialité se réfère aux situations dans lesquelles le contenu du message doit être gardée secrète, dans le cas de l'anonymat, d'autre part, c'est l'identité de l'expéditeur ou du destinataire, qui doit être gardée secrète. De la même façon, en votant, l'anonymat signifie que l'identité de l'électeur associés à chaque vote doit être caché, et non pas le vote lui-même ou le candidat a voté pour. D'autres propriétés remarquables de cette catégorie sont la vie privée et la non-ingérence. Protection des renseignements personnels, il se réfère à la protection de certaines données, telles que le numéro de carte de crédit d'un utilisateur. Non-ingérence signifie qu'un utilisateur bas ne seront pas en mesure d'obtenir des informations sur les activités d'un utilisateur élevés. Une discussion sur la différence entre l'anonymat et d'autres propriétés de dissimulation d'informations peuvent être trouvées dans HO03 [, HO05]. Une caractéristique importante de l'anonymat, c'est qu'il est généralement relative à la capacité de l'observateur. En général, l'activité d'un protocole peut être observé par divers observateurs, di? Vrant dans les informations qu'ils ont accès. La propriété anonymat dépend essentiellement de ce que nous considérons comme observables. À titre d'exemple, dans le cas d'un babillard anonyme, une annonce par un membre du groupe est maintenue anonymes aux autres membres, mais il peut être possible que l'administrateur du conseil d'administration a accès à une information privilégiée qui peut lui permettre de déduire l'identité du membre qui l'a publié. Dans l'anonymat peut être exigée pour un sous-ensemble des agents uniquement. Afin de définir complètement l'anonymat d'un protocole, il est donc nécessaire de préciser ce qui se (s) des membres ont de garder l'anonymat. Une généralisation est le concept de l'anonymat à l'égard d'un groupe: les membres sont divisés en un certain nombre de séries, et nous sommes autorisés à révéler à quel groupe l'utilisateur responsable de l'action appartient, mais pas l'identité de l'utilisateur lui-même. Plusieurs définitions formelles et les cadres d'analyse anonymat ont été développés dans la littérature. Elles peuvent être classifiées en ed approches fondées sur les processus de calculs ([SS96, RS01]), la logique épistémique ([SS99], HO03), et des vues de fonction ([HS04]). La plupart de ces approches sont fondées sur le principe dit de confusion: un système est anonyme si l'ensemble des résultats possibles observable est saturé pour les utilisateurs prévus anonymes. Plus précisément, si dans un calcul le coupable (l'utilisateur qui exécute l'action) est i et le résultat observable est o, alors pour tout autre agent j il doit y avoir un calcul où j est le coupable et l'observable est encore o. Cette approche est aussi appelée possibiliste, et s'appuie sur non-déterminisme. En particulier, les choix probabilistes sont interprétés comme non déterministe. Nous nous référons à RS01] pour plus de détails sur la relation de cette approche à la notion d'anonymat.
3
Yahmadi, Imed. "Vers un calcul pour la spécification et l'analyse des protocoles cryptographiques." Thesis, National Library of Canada = Bibliothèque nationale du Canada, 1998. http://www.collectionscanada.ca/obj/s4/f2/dsk2/ftp04/mq26295.pdf.
Full text
4
Bonet, d'Oléon Karen de. "Spécification et validation du protocole de communication KerNet+." Nantes, 1991. http://www.theses.fr/1991NANT2066.
Full textAbstract:
L'objet du travail présenté ici consiste en la spécification complète d'un protocole de communication, appelé KerNet+, de la couche Application du modèle de référence normalisé par l'ISO pour l'Interconnexion des Systèmes Ouverts. Ce protocole introduit et définit un ensemble de services de communication, mis directement à la disposition des tâches utilisateur des sites communicants et conçus pour s'appliquer spécifiquement aux tâches de conduite et de pilotage en temps réel de procédés industriels continus et manufacturiers complexes. Les hypothèses adoptées pour spécifier le protocole KerNet+ sont que ses services sont destinés à des tâches parallèles, asynchrones et faiblement couplées. La principe de communication de KerNet+ repose sur la coopération par échange de messages et le mode de communication choisi est une extension des concepts de CSP, c'est-à-dire le mode synchrone par rendez-vous, dont on propose une décomposition en deux phases génériques. Il est montré que cette décomposition autorise l'écriture naturelle de synchronisations réputées complexes dans les applications temps réel. Il est proposé une architecture du protocole conforme à la norme ISO 9545 de l'ISO et le protocole est modélisé sous la forme de cinq systèmes de transition parallèles synchronisés. Cette architecture autorise l'utilisation des services de KerNet+ tant dans un contexte réparti que pour faire interagir des tâches résidant sur le même site, la localisation effective des tâches restant transparente à l'utilisateur. Le chapitre 1 est consacré à la présentation du langage CSP et des multiples extensions qui en ont découlé. Le chapitre 2 contient la description des services de communication introduits dans le protocole KerNet+. Le Chapitre 3 propose une structuration des entités fonctionnelles chargées de la réalisation des services de KerNet+ et modélise leur comportement. Le Chapitre 4 présente une spécification formelle du protocole dans le langage normalisé Estelle et son comportement global est vérifié par observation en simulation.
5
Rodriguez, Carlos. "Spécification et validation de systèmes en Xesar." Phd thesis, Grenoble INPG, 1988. http://tel.archives-ouvertes.fr/tel-00326427.
Full textAbstract:
Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés
6
Rieu, Christine. "Outil d'aide à la spécification et à l'implémentation de protocoles de transfert." Clermont-Ferrand 2, 1989. http://www.theses.fr/1989CLF21105.
Full textAbstract:
Une approche de conception est construite à partir d'une classification fonctionnelle des informations manipulées. Un support graphique permet de decrire la communication à réaliser. La technique de description proposée est ensuite vérifiée au moyen d'un logiciel de vérification de systèmes décrits sous forme de réseaux de Petri de type Predicats-Transitions.
7
Romero, Hernandez Ivan. "Modélisation, spécification formelle et vérification de protocoles d'interaction : une approche basée sur les rôles." Grenoble INPG, 2004. http://www.theses.fr/2004INPG0159.
Full textAbstract:
Dans cette thèse nous présentons une approche pour la spécification, modélisation et validation des protocoles d'interaction entre agents réactifs. Cette approche est basée sur la notion de rôle-attribut, telle qu'elle est définie dans les méthodologies orientées agent GAIA et MAD KIT. Les rôles peuvent être vus comme des attributs sociaux assignés aux agents, et qui sont pris dans chaque interaction entre agents pour accomplir la fonctionnalité de l'ensemble, cette approche peut permettre d'envisager la définition de schémas de conduite entre des rôles génériques et les traduire vers un ensemble de comportements concrets. On propose pour vérifier la faisabilité de cette idée, une méthode assistée par ordinateur pour la traduction automatique d'une spécification visuelle représentant des rôles(diagrammes de séquence AUML), vers un modèle formel vérifiable avec un model-checker (PromelalSPIN)Ln this thesis we present an approach for specifying, modelling and validating agent interaction protocols. This approch is based on the notion of role attribute, as it is implied on the agent-oriented methodologies MADKIT and GAIA. Roles could be seen as social attributes of agent groups, that are taken in the context of any given interaction. If we see roles like this, we could also imagine schemes to generate an actual specification with concrete agents from the generic specification using roles. To test this approch we propose a machine-assisted specification process that takes a role definiton expressed on a visual notation (AUML), and generates a formai equivalent on the language Promela
8
Dakroury, Yasser. "Spécification et validation d'un protocole de messagerie multi-serveur pour l'environnement MMS." Nantes, 1990. http://www.theses.fr/1990NANT2041.
Full textAbstract:
On présente un nouveau concept pour l’implémentation du protocole MMS: le protocole de multi-serveur. De sa définition, le protocole multi-serveur MMS envisage une coopération possible entre plusieurs serveurs MMS pour exécuter un service demandé par l'utilisateur client. Ce protocole de multi-serveur nécessite la définition d'un nouveau type d'objet, c'est-à-dire l'objet reparti. Une architecture générale a été introduite pour présenter les interactions possibles entre l'utilisateur client et les serveurs, dits principal et secondaire(s). Cette architecture repose sur le fait que l'objet est considéré comme un agent actif qui peut communiquer avec la fonction opératoire du serveur. L'objet liste de variables et l'objet tache ont été choisis pour être traités par ce protocole de multi-serveur. Les spécifications du protocole sont présentées par des automates d'états finis. Ensuite, ces automates ont été validés à l'aide du système auto en utilisant les algèbres de processus communicants.
9
Auriol, Guillaume. "Spécification et implémentation d'une architecture de signalisation à gestion automatique de la QdS dans un environnement IP multi domaines." Toulouse, INSA, 2004. http://www.theses.fr/2004ISAT0029.
Full textAbstract:
L’Internet du futur aura à transporter les données de nouvelles applications avec des garanties de qualité de service (QdS). De ce besoin résulte la nécessité d’en re-concevoir l’architecture. Par ailleurs, la structure de l’Internet, composé de domaines indépendants vis à vis de la gestion de la QdS, pose le problème de la continuité du service lors de la traversée de plusieurs domaines. Face à ces deux problématiques, la thèse soutenue est celle d’un système de communication offrant des garanties de QdS par flux applicatif dans un environnement Internet multi domaines. Son architecture intègre un plan communication comportant plusieurs services/protocoles aux niveaux Transport et IP, et un plan signalisation assurant la gestion des ressources à la frontière des domaines. Nos contributions sont les suivantes. Nous proposons un modèle de caractérisation des services IP et Transport, étayé par : (1) des mesures réalisées sur une plate forme nationale, (2) une étude en simulation (ns-2) et (3) des mesures réalisées sur une plate-forme émulant (Dummynet) un Internet multi domaines. Nous étendons l’architecture de communication proposée dans des travaux antérieurs de façon à abstraire le niveau applicatif de la complexité du choix des services Transport et IP, et à optimiser l’utilisation des ressources du réseau. Nous spécifions en UML et implémentons en Java notre proposition d’architecture de signalisation permettant d’assurer la continuité du service offert aux applications sur tous les domaines traversés. Enfin, nous testons le système de communication avec deux types d’applications multimédias sur une plate-forme émulant le comportement de plusieurs domaines DiffServThe future Internet will have to transport the new application data with Quality of Service (QoS) guarantees. Then, it is necessary to redesign its architecture. In other respect, by definition, the Internet consists of several autonomous domains with their own QoS management mechanisms. This last point raises the question to carry the service continuity over all the domains. Then, to solve these two precedent problems the work presented in this thesis proposes a communication system providing guarantees of QoS in a multi-domain environment. This system is composed of both a communication plane and a signaling plane. The first one provides multi IP and Transport services when the second one manages the resources between the involved domains. Our contributions are the following ones. Firstly, we propose a model to characterize the IP and Transport services based on experiments over a national platform, ns-2 simulations and measurements performed over a DiffServ multi-domain emulation platform. Then, we upgrade a previous proposed communication architecture integrating this model to simplify the user task. Actually, the system is able to select automatically the appropriated Transport and IP services to satisfy the users. Secondly, we specify in UML and we implement in Java our signaling architecture providing the guarantee of the service continuity over all involved domains. Finally, we test, by the mean of two kinds of application, the complete system over a platform which emulates the behavior of several DiffServ domains
10
Jacinto, Montes Ricardo R. "Protocoles de validation à deux phases dans les systèmes transactionnels répartis : spécification, modélisation et vérification." Toulouse 3, 1995. http://www.theses.fr/1995TOU30050.
Full textAbstract:
Assurer la coherence des donnees dans un traitement reparti est un probleme majeur qui a besoin, pour etre resolu, de la definition des regles de fonctionnement precises. Dans ce contexte, l'osi a defini le protocole iso-tp (transaction processing) pour la realisation des traitements transactionnels repartis. Iso-tp est un protocole a controle centralise base sur une structure hierarchique arborescente qui s'appuie sur la fonction ccr (commitment concurrency & recovery) afin d'assurer la coherence des relations bipoint qui composent l'arbre transactionnel. Pour maitriser la complexite des mecanismes specifies dans iso-tp, nous avons defini une methodologie de modelisation et verification structuree fondee sur la decomposition (recursive) d'un systeme en sous-systemes et sur les niveaux d'abstraction. Le protocole iso-tp est tres bien adapte pour les applications tels que les systemes de gestion de bases de donnees repartis (sgbdr). Cependant le couplage des mecanismes de iso-tp et du sgbdr fait ressortir une complexite qui, pour etre maitrisee, necessite d'une methodologie de conception. Dans ce but une methodologie fondee sur la complementarite de deux techniques de description formelle (reseaux predicat/transition etiquetes et estelle) a ete developpee pour guider la conception d'un sgbdr reel. La constante evolution technologique conduit au developpement d'applications qui s'appuient sur le concept de travail cooperatif. Ce type d'applications induit de nouveaux besoins en termes de protocoles de validation. Pour repondre a ces besoins un protocole fonde sur les concepts d'initiation repartie et de coordonnateur dynamique a ete defini. Ce protocole permet d'assurer: l'adaptation a toute topologie de travail, l'independance par rapport a un site particulier et la diminution du temps de validation
11
Andrey, Laurent. "Protocoles de communication et grammaires attribuées." Nancy 1, 1993. http://www.theses.fr/1993NAN10083.
Full textAbstract:
Le but de l'étude est d'examiner l'adéquation des grammaires attribuées pour décrire formellement des protocoles de communication et pour en dériver quasi-automatiquement une implantation d'une entité de protocole. Les protocoles considérés sont ceux des couches basses du modèle OSI, et l'utilité de telles descriptions formelles est placée dans le contexte général de l'ingénierie des protocoles. La contribution personnelle consiste en une proposition du formalisme GAPP (grammaires attribuées pour les protocoles) basée sur les travaux existants en intégrant des idées issues des applications traditionnelles des grammaires attribuées en compilation. Dans GAPP, les règles de production servent à décrire la partie contrôle d'un protocole. Les terminaux représentent les interactions (primitives de service, unîtes de donnée, time-out) qu'échange le protocole avec l'extérieur. Les attributs permettent de relier les interactions entre elles, et d'incorporer le contexte dans la grammaire par l'intermédiaire de gardes sur les productions. L'exemple normalisé abracadabra est traité. Des extensions comme le multiplexage sont abordées
12
Talbi, Mehdi. "Spécification et vérification automatique des propriétés des protocoles de vote électronique en utilisant la logique ADM." Rennes 1, 2010. http://www.theses.fr/2010REN1S073.
Full textAbstract:
Les systèmes de vote électronique sont basés sur des protocoles cryptographiques faisant usage de primitives avancées (chiffrement homomorphe, signature en aveugle, etc. ) et impliquant des canaux de communication élaborés (anonymes, privés) dans le but de garantir certaines propriétés de sécurité : éligibilité, équité, anonymat, etc. Pour les systèmes critiques tels que celui du vote électronique, l’usage des méthodes formelles, pour prouver que les propriétés prétendues satisfaites par un protocole sont réellement garanties, devrait être incontournable. Dans cette thèse, nous proposons d’utiliser la logique modale ADM afin de spécifier une sélection de propriétés de sécurité. Ces propriétés sont vérifiables par rapport à un modèle à base de traces représentant des exécutions valides du protocole. Notre modélisation des protocoles tient en compte de la présence d’un intrus actif dont le pouvoir de déduction est ajusté en fonction des spécificités introduites par le vote électronique. La modélisation des protocoles et la spécification des propriétés sont appuyées par une étude de cas portant sur le protocole de vote FOO dont nous proposons une analyse de sa sécurité. En complément, nous proposons d’exploiter le système de preuve qui accompagne la logique ADM, afin d’implémenter un outil permettant d’automatiser le processus de la vérification formelle des propriétés spécifiées par rapport aux traces du protocole analyséIt is a well known fact that only formal methods can provide a proof that a given system meets its requirements. Their use should be mandatory for critical systems such as electronic voting. In this thesis, we propose the use of the modal and linear ADM logic in order to specify a set of security properties that a voting protocol is required to satisfy : eligibility, non-reusability, accuracy, fairness, anonymity, receipt-freeness, etc. Our goal is to check these properties against a trace-based model where a trace represents a valid run of the protocol. Protocol executions take place in a hostile environment controlled by an active intruder whose deduction power is incremented according to electronic voting cryptographic primitives (blind signature, bit-commitment, homomorphic encryption, zero-knowledge proof, etc. ). Protocol modeling and properties specification are applied to the FOO protocol as a case study. Additionally, we propose to exploit the tableau-based proof system of the ADM logic, in order to develop a tool enabling the automatic verification of security properties against selected traces of the analyzed protocol
13
Dupeux, Arnaud. "Spécification et implantation de protocoles OSI : une expérience de la couche transport dans le langage ADA." Bordeaux 1, 1986. http://www.theses.fr/1986BOR10527.
Full textAbstract:
Validation des protocoles, amelioration des algorithmes existants. Specification et description detaillees d'une entite de transport osi, gestion des conflits et des evenements, proposition d'un modele. Langage ada et ses possibilites pour exprimer des phenomenes paralleles; application: programmation de l'architecture de la couche transport osi
14
Zwecker, Stella. "Représentation et spécification d'architectures d'interconnexion de réseaux hétérogènes vers la définition d'une base de connaissances." Toulouse 3, 1993. http://www.theses.fr/1993TOU30052.
Full textAbstract:
L'objet de cette these est de definir une methodologie pour la specification d'architectures d'interconnexion de reseaux heterogenes, et d'integrer cette methodologie au sein d'un systeme base sur l'utilisation de techniques d'intelligence artificielle. La methodologie permet: 1) d'evaluer l'incompatibilite des reseaux a interconnecter (lorsque des adressages et/ou les couples service-protocole d'une couche sont incompatibles, les entites de cette couche sont incapables de s'identifier et/ou de dialoguer), 2) de realiser une specification orientee fiabilite de l'architecture d'interconnexion resultante (les deux techniques proposees, la conversion et l'encapsulation, permettent de controler les incompatibilites des reseaux a partir d'une certaine couche de leur architecture). Pour integrer la methodologie au sein d'un systeme a base de connaissances, les differents concepts mis en jeu ont ete representes (en particulier une modelisation generale des adressages au sein d'une architecture multi-couches a ete definie). Le prototype implante combine deux formalismes de representation des connaissances (formalisme oriente objets; langage prolog). Ce systeme met en oeuvre des sessions interactives, qui fournissent a un utilisateur des guides pedagogiques pour l'etude de cas d'interconnexion de reseaux: par exemple reseaux longue distance de type x25 ou ip (i. E. Dont la couche reseau est avec ou sans connexion); reseaux locaux de type ieee 802 sans couche reseau, etc.
15
Ayoub, Dit Ayadi Mohamed. "Contribution à la spécification formelle et vérification d'architectures de communication pour les transactions distribuées (couches hautes du modèle de référence OSI DE L'ISO)." Toulouse 3, 1990. http://www.theses.fr/1990TOU30118.
Full textAbstract:
Les travaux presentes dans ce memoire portent sur la specification formelle et l'analyse des mecanismes commitment concurrency recovery (ccr) et transaction processing (tp) de la couche application du modele osi de l'iso pour les reseaux d'ordinateurs. Ces mecanismes permettent la realisation d'actions atomiques sur des liaisons bipoints (ccr) et dans un contexte arborescent (tp). Deux techniques complementaires de description formelle sont utilisees: le modele reseaux de petri etiquete (rpte) et le langage estelle. La modelisation de la fonction ccr au moyen du modele rpte a montre en particulier, la necessite, d'une part, de specifier une phase dite d'initialisation de la relation ccr (distribution dynamique des roles superieur et subordonne) et, d'autre part, de definir une nouvelle primitive de service. La specification au moyen du langage estelle d'une architecture transactionnelle a montre, en particulier, l'interet de ce langage pour la specification d'une architecture complexe (comportant cinq niveaux de fonctionnalites du modele osi de l'iso: presentation - ccr ase - tp ase - sacf-macf)
16
Garnier, Gérard. "Modélisation de protocoles : application à la couche liaison de données de F.I.P." Nancy 1, 1992. http://www.theses.fr/1992NAN10308.
Full textAbstract:
Les architectures multicouches de protocoles et de services, basées sur le modèle de référence de l'O. S. I. (open systems interconnection) font appel à de nombreux et complexes mécanismes dont il est absolument nécessaire de spécifier le comportement de manière complète et non ambigüe. Seule une approche fondée sur une technique de description formelle permet de satisfaire à cet objectif. L'utilisation d'une telle approche permet en outre d'effectuer une majorité des vérifications et validations, au cours de l'élaboration même d'un cahier des charges ou de la conception d'un système. En conséquence, le premier chapitre de ce mémoire, après un bref rappel de la terminologie définie dans le modèle O. S. I. , expose une synthèse des techniques de description formelle, applicables aux protocoles et services I. S. O. (international standard organization). Le deuxième chapitre est consacré à la définition d'un outil de spécification, pour la modélisation des protocoles, à partir du grafcet et de concepts et possibilités d'expression provenant des langages informatiques. L'objectif du troisième chapitre est d'illustrer l'utilisation de l'outil proposé dans le chapitre précédent, de manière à montrer son applicabilité à la description formelle de protocoles. L'exemple choisi est la couche liaison de données du bus de terrain F. I. P. (flux information processus). La conclusion de ce mémoire porte sur l'avenir de l'outil proposé ainsi que sur les extensions dont il doit bénéficier
17
Saad, Khorchef Fares. "Cadre Formel pour le Test de Robustesse des Protocoles de Communication." Phd thesis, Université Sciences et Technologies - Bordeaux I, 2006. http://tel.archives-ouvertes.fr/tel-00138202.
Full textAbstract:
Dans le domaine des télécommunications, il est indispensable de valider rigoureusement les protocoles avant de les mettre en service. Ainsi, il faut non seulement tester la conformité d'un protocole, mais il s'avère aussi nécessaire de tester sa robustesse face àdes événements imprévus. La littérature concernant le test de robustesse est beaucoup moins conséquente que le test de conformité. A travers ce document, nous considérons la définition de la robustesse suivante : "la capacité d'un système, conforme à sa spécification nominale, à adopter un comportement acceptable en présence d'aléas". Notre approche se fonde sur l'analyse du comportement du système face à des aléas. On considérera comme aléa tout événement non prévu amenant le système à une impossibilité temporaire ou définitive d'exécuter une action. Les contributions principales de ce document sont brièvement présentées ci-dessous :
(1) Proposition d'un cadre formel comportant une approche, une relation de robustesse et méthode pour générer les cas de test de robustesse d'un système modélisé sous forme d'IOLTS. Notre approche comporte deux méthodes :
- La méthode TRACOR (Test de Robustesse en présence d'Aléas COntrôlables et Représentables) consiste à vérifier la robustesse d'un système en présence d'aléas contrôlables et représentables. Cette méthode intègre les entrées invalides, entrées inopportunes, sorties
acceptables et traces de blocage dans la spécification nominale, pour obtenir une spécification augmentée. Cette dernière servira de base pour la génération de séquences de test de robustesse.
- La méthode TRACON (Test de Robustesse en présence d'Aléas COntrôlables et Non représentables) est focalisée sur le test de robustesse en présence d'aléas contrôlables et non représentables. Elle consiste à enrichir la spécification nominale par les sorties acceptables et les traces de suspension afin d'obtenir la spécification semi-augmentée. Cette dernière servira de base pour la génération de séquences de test de robustesse.
(2) Pour formaliser la robustesse d'une implémentation vis-à-vis de la spécification augmentée (ou la spécification semi-augmentée), nous proposons une relation binaire, appelée "Robust", basée sur l'observation des sorties et blocages de l'implémentation après l'exécution de traces comportant les aléas.
(3) Afin de générer les cas de test de robustesse, nous proposons une méthode basée sur un coloriage de la spécification augmentée (ou la spécification semi-augmentée) et un ensemble d'objectifs de test de robustesse.
(4) Les fondements de notre approche sont implémentés dans l'outil RTCG. Cette application offre trois interfaces. La première et la deuxième permettent d'automatiser la méthode TRACOR. La troisième interface permet d'automatiser la méthode TRACON.
(5) Une étude de cas, sur les protocoles SSL handshake et TCP, montrant une évaluation
pratique de notre approche.
18
Elabd, Emad. "Conformité de services Web par rapport à des spécifications de haut niveau." Phd thesis, Université Claude Bernard - Lyon I, 2011. http://tel.archives-ouvertes.fr/tel-00867892.
Full textAbstract:
Actuellement, la technologie des services Web évolue rapidement, en étant soutenue par les grands acteurs du domaine des systèmes d'information. Les applications basés sur services Web sont faiblement couplées et utilisables de façon automatique via l'utilisation d'un ensemble de normes basées sur XML. Hormis la description syntaxique des messages, il est nécessaire d'avoir une description sémantique du comportement des services. En effet, lors de la conception d'un service ou lors d'une composition de services, il est important de vérifier la conformité avec un cahier des charges. L'enrichissement des descriptions des services par l'inclusion de leurs comportements est de plus en plus important. Ce comportement peut être décrit par des protocoles métier représentant les séquences possibles d'échanges de messages. Les services Web utilisent des politiques de contrôle d'accès (ACP) pour restreindre l'accès à des consommateurs autorisés. Ces politiques doivent faire partie de la description du service. Dans cette thèse, l'analyse d'interopérabilité en termes de contrôle d'accès après la formalisation des services Web annotés avec les politiques de contrôle d'accès est réalisée. Nous présentons une approche pour intégrer les outils de vérification dans l'architecture de contrôle d'accès de façon à garantir une interaction sans erreurs. Les politiques et les crédits sont présentés comme une ontologie afin de bénéficier de la flexibilité offerte par subsomption sur des concepts. La chorégraphie des services Web est utilisée dans la phase de conception d'applications pair à pair complexes dans lesquelles chaque pair peut être implémenté par un service Web. Par conséquent, la sélection des services Web pour l'implémentation de chorégraphie en utilisant l'approche de vérification de compatibilité avec contrôle d'accès est l'un des objectifs de notre recherche. Dans ce travail, les modèles de protocole métier du service Web sont étendus en ajoutant des informations au message sur chaque transition du service dans lequel ce message sera envoyé ou reçu. Nous définissons et vérifions la compatibilité des services Web afin de voir si (et comment) plusieurs services peuvent avoir des interactions en fonction de leurs protocoles. Cette approche aidera les concepteurs à choisir des services Web de manière simple et à vérifier s'ils peuvent mettre en œuvre la chorégraphie nécessaire en vérifiant la compatibilité avec notre approche.
19
Amyay, Omar. "Méthodologie de spécification d'activités de communication dans une architecture multi-couches vers la définition d'une base de connaissances." Toulouse 3, 1991. http://www.theses.fr/1991TOU30209.
Full textAbstract:
La specification des services et protocoles de communication dans une architecture multi-couches, de type osi, est une problematique essentielle dans le contexte de la conception de reseaux d'ordinateurs. Il s'agit d'obtenir, a partir d'un ensemble de contraintes dites donnees initiales qui caracterisent le probleme pose, une specification operationnelle du couple service-protocole d'une couche donnee. Une methodologie de resolution de cette problematique a ete definie en termes d'etapes de synthese et de verification. La planification de ces etapes constitue une trajectoire de specification. Celle-ci se base sur l'integration progressive des contraintes donnees initiales et la verification de la specification issue de chaque etape de synthese par des contraintes de validite qui caracterisent une solution admissible. Deux types de trajectoires ont ete proposes, selon le style de la specification initiale du couple service-protocole: type operationnel et point de vue fournisseur du service; type oriente proprietes de connaissance et point de vue utilisateurs du service. Les activites de synthese et de verification ont ete elaborees pour ces deux trajectoires et formalisees en termes de systemes de transitions etiquettees, de logique temporelle et de logique epistemique. L'originalite de la deuxieme trajectoire de specification et l'utilisation de la logique epistemique ont ete mises en evidence. Une approche intelligence artificielle a permis de definir un modele conceptuel d'un systeme a base de connaissances pour la mise en uvre de la methodologie proposee. Il est structure selon trois niveaux de representation des connaissances relatifs au domaine, au raisonnement caracterisant les activites de synthese et de verification et a la planification des etapes d'une trajectoire de specification
20
Elabd, Emad. "Compliance of Web services over a high level specification." Thesis, Lyon 1, 2011. http://www.theses.fr/2011LYO10122/document.
Full textAbstract:
Actuellement, la technologie des services Web évolue rapidement, en étant soutenue par les grands acteurs du domaine des systèmes d'information. Les applications basés sur services Web sont faiblement couplées et utilisables de façon automatique via l'utilisation d'un ensemble de normes basées sur XML. Hormis la description syntaxique des messages, il est nécessaire d’avoir une description sémantique du comportement des services. En effet, lors de la conception d'un service ou lors d'une composition de services, il est important de vérifier la conformité avec un cahier des charges. L’enrichissement des descriptions des services par l’inclusion de leurs comportements est de plus en plus important. Ce comportement peut être décrit par des protocoles métier représentant les séquences possibles d'échanges de messages. Les services Web utilisent des politiques de contrôle d'accès (ACP) pour restreindre l'accès à des consommateurs autorisés. Ces politiques doivent faire partie de la description du service. Dans cette thèse, l'analyse d'interopérabilité en termes de contrôle d’accès après la formalisation des services Web annotés avec les politiques de contrôle d’accès est réalisée. Nous présentons une approche pour intégrer les outils de vérification dans l'architecture de contrôle d’accès de façon à garantir une interaction sans erreurs. Les politiques et les crédits sont présentés comme une ontologie afin de bénéficier de la flexibilité offerte par subsomption sur des concepts. La chorégraphie des services Web est utilisée dans la phase de conception d’applications pair à pair complexes dans lesquelles chaque pair peut être implémenté par un service Web. Par conséquent, la sélection des services Web pour l’implémentation de chorégraphie en utilisant l’approche de vérification de compatibilité avec contrôle d'accès est l'un des objectifs de notre recherche. Dans ce travail, les modèles de protocole métier du service Web sont étendus en ajoutant des informations au message sur chaque transition du service dans lequel ce message sera envoyé ou reçu. Nous définissons et vérifions la compatibilité des services Web afin de voir si (et comment) plusieurs services peuvent avoir des interactions en fonction de leurs protocoles. Cette approche aidera les concepteurs à choisir des services Web de manière simple et à vérifier s’ils peuvent mettre en œuvre la chorégraphie nécessaire en vérifiant la compatibilité avec notre approcheCurrently, Web services technology is rapidly move forward supported by major players in the field of information systems. Web services applications are loosely coupled and usable in an automatic way via the use of a set of standards based on XML. Beside the syntactic description of messages, there is a need for the semantic description of the behavior of services. Indeed, whether in the design of a service or composition of services, it is important to check compliance with a set of specifications. Enriching services descriptions by including their behaviors is becoming more and more important. This behavior can be described by business protocols representing the possible sequences of message exchanges. Web services use access control policies (ACP) to restrict the access to authorized consumer. These policies should be a part of the service description. In this thesis, the interoperability analysis in terms of AC after the formalization of the Web services annotated with the access control (AC) is performed. In addition, we present an approach for embedding the checking tools in the AC enforcement architecture to guarantee the errors free interaction. The ACP and the credentials are presented as ontology in order to benefit from the flexibility offered by subsumption on concepts. Web services choreography is used in the design phase of complex peer-to-peer applications in which each peer can be implemented by a Web service. Therefore, selecting Web services for choreography implementation using the compatibility checking approach with access control is one of the objectives of our research. In this work, the business protocol models of the Web service are extended by adding information to the message on each transition about the service in which this message will sent to or received from. We define and verify Web service compatibility in order to see if (and how) several services can have interactions based on their protocols. This approach will help the designers to select Web services in an easy way and verify if they can implement the required choreography or not by checking the compatibly using our approach
21
Bhatia, Sapan. "Optimisations de compilateur optimistes pour les systèmes réseaux." Bordeaux 1, 2006. http://www.theses.fr/2006BOR13169.
Full textAbstract:
Cette thèse présente un ensemble de techniques qui permettent l'optimisation des performances des systèmes réseaux modernes. Ces techniques reposent sur l'analyse et la transformation des programmes impliqués dans la mise en oeuvre des protocoles réseaux. La première de ces techniques fait appel à la spécialisation de programmes pour optimiser des piles de protocoles réseaux. La deuxième, que nous avons nommée spécialisation distante, permet à des systèmes embarqués limités en ressources de bénéficier de la pécialisation de programmes en déportant à travers le réseaux les opérations de spécialistion à une machine distante moins limitée. La troisième propose un nouvel allocateur de mémoire qui optimise l'utilisation des chaches matériels faite par un serveur réseau. Enfin, la quatrième utilise l'analyse de programmes statiques pour intégrer l'allocateur proposé dans un serveur réseau existant. On appelle ces techniques optimisations compilateur parce qu'elles opèrent sur le flot des données et du contrôle dans des programmes en les transformant pour qu'ils fonctionnent plus efficacement.
22
Lambolais, Thomas. "Modélisation du développement de spécifications LOTOS." Vandoeuvre-les-Nancy, INPL, 1997. http://www.theses.fr/1997INPL106N.
Full textAbstract:
Notre travail s'inscrit dans les premières étapes du développement de logiciels concernant le passage d'un cahier des charges à une spécification formelle, dans le domaine des réseaux de télécommunications. Notre sujet consiste à étudier la modélisation des étapes de développement de spécifications en langage LOTOS. Le modèle utilisé, PROPLANE, a été préalablement établi pour d'autres domaines. Par le biais d'un nouveau domaine d'application, l'objectif à long terme de notre étude est d'évaluer le modèle PROPLANE et de proposer des améliorations si nécessaire. LOTOS est constitué d'une algèbre de processus et d'une algèbre de données. Nous nous sommes concentrés sur la construction des expressions de comportement, c'est-à-dire des processus, en ayant éventuellement recours aux données. Sous le modèle PROPLANE, toute évolution d'un développement est gérée par des operateurs de développement. Notre modélisation correspond ainsi à des définitions d'operateurs pouvant s'enchainer les uns aux autres. Nous distinguons les constructions architecturale et, comportementale, pour lesquelles les mécanismes utilisés en LOTOS diffèrent. L’architecture fait une large utilisation des operateurs de composition parallèle, avec lesquels il faut veiller à conserver des processus effectifs, voire réguliers. Nous définissons pour cela des notions telles que la rigidité. La construction comportementale demande de définir des opérateurs permettant de gérer le développement d'arbres de transitions, ainsi que le détail de ces transitions. La nouveauté de notre approche consiste à chercher à profiter des propriétés sémantiques des processus en cours de développement. Afin de supporter des lignes de construction incrémentale par réduction de l'indéterminisme, nous donnons une définition opérationnelle des relations d'extension et de réduction de processus. Il apparait que PROPLANE doit être étendu pour manipuler des propriétés temporelles sur les états de développement.
23
Viho, Gagnon Gbédé. "Une contribution à la suppression des anomalies dans les protocoles de communication." Bordeaux 1, 1991. http://www.theses.fr/1991BOR10573.
Full textAbstract:
Actuellement, plusieurs methodes et outils permettent de specifier les protocoles de communication et d'y detecter les anomalies. Cependant, peu de methodes sont developpees pour supprimer ces anomalies. Dans cette these, nous proposons: 1) une methode de synthese qui guide la specification et evite l'occurrence des receptions non specifiees et des transitions non executables; 2) deux methodes qui interviennent apres detection des anomalies et proposent des solutions pour supprimer les receptions non specifiees, les deadlocks et les boucles bloquantes. Les outils developpes mettant en uvre ces methodes sont egalement presentes
24
Allouis, Tristan. "Spécification de paramètres techniques et stratégie d'échantillonnage pour la conception de nouveaux capteurs lidars dédiés à la cartographie de forêts." Thesis, Paris, AgroParisTech, 2011. http://www.theses.fr/2011AGPT0086/document.
Full textAbstract:
Les forestiers ont besoin d'outils permettant de cartographier les essences, la hauteur, la structure ou la biomasse des peuplements. Même si le lidar aéroporté (light detection and ranging, détection et télémétrie par laser) ne permet pas de mesurer l'ensemble de ces variables, il permet d'accéder aux hauteurs et à la biomasse de manière rapide, précise et surtout spatialisée sur de grandes surfaces. Cependant, les lidars aujourd'hui utilisés en forêts n'ont pas été conçus spécifiquement pour étudier la végétation, et l'ajustement de leurs caractéristiques techniques est supposé permettre d'améliorer la précision des mesures. L'objectif de cette thèse est de déterminer des configurations de capteurs lidars dédiés à l'étude de la végétation forestière, et de proposer des méthodes d'extraction de paramètres forestiers adaptés aux différentes configurations. La capacité de différentes résolutions (taille d'empreinte et échantillonnage spatial), longueurs d'onde et modes d'enregistrement du signal retour à mesurer des paramètres forestiers (hauteurs et densité d'arbres, taille des couronnes et indirectement volume et biomasse) a été évaluée. Les études ont été menées de l'échelle de l'arbre jusqu'à celle du peuplement, sur des données expérimentales ou simulées. Dans une première partie, des méthodes de traitement de données lidars aéroportés classiques (scanneur, largeur du faisceau décimétrique, 5 mesures/m², laser proche infrarouge) ont été développées pour estimation la biomasse d'arbres individuels. Dans cette étude, l'apport de nouvelles données dites "full-waveform" (enregistrement du signal complet) a été démontré par rapport aux traditionnelles données multiéchos (extraction des échos les plus significatifs). Dans une seconde partie, une expérimentation avec un prototype lidar du Commissariat à l'Énergie Atomique (CEA) embarqué sur un ULM a été réalisée (profileur, largeur de faisceau de 2,4 m, espacement de 2,4 m entre deux mesures successives le long de la ligne de vol, laser ultraviolet). Sans permettre des mesures d'arbres individuels, cette configuration de capteur a permis d'étudier les variations de la structure des arbres à l'intérieur d'une placette forestière (30 m de diamètre). En validant l'utilisation d'un laser ultraviolet pour l'étude de la végétation, les résultats de cette expérience permettent d'envisager le développement de capteurs bifonctions atmosphère/végétation. Dans une troisième partie, des signaux lidars à larges empreintes (plusieurs dizaines de mètres au sol) ont été simulés par agrégation de signaux lidars aéroportés classiques. Une méthode de modélisation permettant d'étudier la dynamique supposée d'un signal lidar satellitaire dans différents types de forêts a été proposée. Elle apporte des informations utiles à la calibration de l'énergie à émettre pour une future mission satellitaire dédiée à la cartographie de forêts. Le principal problème avec les données à larges d'empreintes est la forte influence de la topographie sur la précision des mesures de hauteurs d'arbres en zones pentues. En conséquence, une méthode de correction de cet effet a été élaborée, permettant ainsi de mesurer les hauteurs d'arbres avec une précision jusqu'alors inenvisageable. Cette méthode a de plus ouvert de nouvelles perspectives dans l'estimation de la topographie sous la forêt, à partir de données lidars à larges empreintesForesters need tools to map the tree species, tree heights, stand structure and biomass. Although the airborne lidar (Light detection and ranging) technology does not give access to all these variables, it can provide quick, accurate and spatially explicit measurements of tree heights and biomass over large surfaces. However, lidar systems currently used have not been specially designed to performed vegetation studies. The adjustment of the technical characteristics of such systems is expected to improve the accuracy of retrieved forest parameters. Consequently, the objective of this thesis is to determine configurations of lidar sensors dedicated to the study of forest vegetation, and to propose methods designed to extract forest parameters depending on the different configurations. The ability of different resolutions (footprint size and spatial sampling), wavelengths and sampling modes of the backscattered signal to measure forest parameters (canopy height and density, crown size and also volume and biomass) was evaluated. The studies were conducted from tree to stand level, on experimental or simulated data. In a first part, we developed methods to process classic airborne lidar data (scanner system, tens of centimeter footprint, 5 measurements/m², near-infrared laser) for the estimation of the biomass of individual trees. In this study, we demonstrated the contribution of new data called "Full-waveform" (recording the entire signal) compared to traditional multi-echoes data (extraction of the most significant echoes). In a second part, we performed an experiment using a Comissariat of Energy Atomique (CEA)'s lidar prototype onboard an ultra-light aircraft (profiler system, 2.4 m footprint, 2.4 m spacing between two measurements along the flight line, ultraviolet laser). Such a configuration did not allow to measure individual trees, but we were able to study variations in forest structure at the plot level (30 m diameter). Having demonstrated the ability of an ultraviolet lidar to perform vegetation studies, this sensor opens the way to the development of bi-functional lidar for both atmosphere and vegetation remote sensing. In a third part, large footprint lidar signals (tens of meters on the ground) were simulated from the aggregation of classical airborne lidar signals. We proposed a method for modeling the signal dynamics of satellite lidars in different forest types, in order to calibrate the energy to emit for a future space-borne mission. The main problem with large-footprint size is the strong influence of topography on accurate measurements of tree heights in steep areas. We consequently developed a method to correct this effect, thus increasing the accuracy of tree height retrieval. This approach also opened new perspectives in topography assessment from large-footprint data in forest environments
25
Dridi, Khaled. "Spécification du protocole MAC pour les réseaux IEEE 802.11e à différentiation de services sous contrainte de mobilité." Thesis, Paris Est, 2011. http://www.theses.fr/2011PEST1016/document.
Full textAbstract:
Cette thèse a pour objectif de proposer de nouvelles approches d'ordonnancement, de coopération et de gestion de la mobilité dans les réseaux sans fil de type IEEE 802.11. Le maintien de la qualité de service (QoS), au niveau MAC, représente la caractéristique fondamentale de ces approches. L'analyse des mécanismes existants nous a conduits à retenir le protocole EDCF, supportant la QoS, comme une base de travail pour l'ensemble de nos propositions. Dans le but de pallier certaines faiblesses du standard 802.11, une nouvelle architecture à base de multi-ordonnanceurs HCF-T, est proposée. Les performances obtenues sont exprimées en termes de gestion du trafic, de maintien du débit, d'élimination de collisions et de réduction de la charge du réseau. Ensuite, un schéma coopératif est présenté et analysé. Il comporte une étude de deux protocoles de relayage AAF et DAF ainsi qu'une évaluation d'un ensemble de techniques de combinaison au niveau du récepteur. Concernant la problématique de la mobilité, nous avons retenu et analysé un scénario prenant en considération les différentes situations rencontrées dans un modèle réel. Un algorithme de résolution multi-couvertures est proposé afin de traiter l'accès dans les zones de recouvrement. Cette étude a mené à distinguer trois régimes de mobilité : faible, moyen et fort. Les performances sont évaluées en fonction des métriques MAC et pour chaque mode de mobilité, un schéma de synthèse est établiThis thesis proposes a new approach relating to the packets scheduling algorithm, the cooperation scheme and the nodes' mobility for IEEE 802.11 wireless network family. Considering the QoS delivery process at the MAC level consists the main feature of the proposal research study. The analysis of the current mechanisms leads to keep the protocol EDCF as the basic model for our work platform. In order to overcome the weakness of the earlier 802.11 standard, a new model based on multi-scheduler algorithm, called HCF-T, is proposed. The achieved performances are summarized following several criteria: traffic control, throughput improving, collisions avoidance, and network load decreasing. Furthermore, in the way of getting better results according to the PHY layer, we presented and analyzed a model of cooperative diversity scheme. It included a couple of relaying protocols AAF and DAF supported by a set of combining techniques to backup the signal at the receiver. To support node's mobility within EDCF, we built-up a model of WLAN which able to track node motion and control the access as in real condition. In the case of overlapping APs ranges, we developed a Multi-coverage algorithm aiming to carry out the session associations. As a result, three levels (Low, Medium, and High) of node's speed are discerned. Finally, EDCF has been implemented on various static and dynamic scenarios. The performances, based on the main MAC-layer metrics, such as throughput, End-2-End delay, and jitter, have been classified and comprehensively evaluated
26
Corrales, Juan-Carlos. "Appariement de spécifications de comportements pour la découverte de services." Phd thesis, Université de Versailles-Saint Quentin en Yvelines, 2008. http://tel.archives-ouvertes.fr/tel-00323970.
Full textAbstract:
The capability to easily find useful services (software applications, software components, scientific computations) becomes increasingly critical in several fields. Current approaches for services retrieval are mostly limited to the matching of their inputs/outputs possibly enhanced with some ontological knowledge. Recent works have demonstrated that this approach is not sufficient to discover relevant components. In this dissertation we argue that, in many situations, the service discovery should be based on the specification of service behavior. The idea behind it, is to develop matching techniques that operate on behavior models and allow delivery of partial matches and evaluation of semantic distance between these matches and the user requirements. Consequently, even if a service satisfying exactly the user requirements does not exist, the most similar ones will be retrieved and proposed for reuse by extension or modification. To do so, we reduce the problem of behavioral matching to a graph matching problem and we adapt existing algorithms for this purpose. Motivated by these concerns, we developed the WS-BeM platform for ranking web services based on behavior matchmaking, which takes as input two WSCL or BPEL protocols and evaluates the semantic distance between them. The prototype is also available as a web service. Furthermore, an application is described concerning the tool for evaluating the effectiveness of the behavioral matchmaking method.
27
Dridi, Khaled, and Khaled Dridi. "Spécification du protocole MAC pour les réseaux IEEE 802.11e à différentiation de services sous contrainte de mobilité." Phd thesis, Université Paris-Est, 2011. http://tel.archives-ouvertes.fr/tel-00681041.
Full textAbstract:
Cette thèse a pour objectif de proposer de nouvelles approches d'ordonnancement, de coopération et de gestion de la mobilité dans les réseaux sans fil de type IEEE 802.11. Le maintien de la qualité de service (QoS), au niveau MAC, représente la caractéristique fondamentale de ces approches. L'analyse des mécanismes existants nous a conduits à retenir le protocole EDCF, supportant la QoS, comme une base de travail pour l'ensemble de nos propositions. Dans le but de pallier certaines faiblesses du standard 802.11, une nouvelle architecture à base de multi-ordonnanceurs HCF-T, est proposée. Les performances obtenues sont exprimées en termes de gestion du trafic, de maintien du débit, d'élimination de collisions et de réduction de la charge du réseau. Ensuite, un schéma coopératif est présenté et analysé. Il comporte une étude de deux protocoles de relayage AAF et DAF ainsi qu'une évaluation d'un ensemble de techniques de combinaison au niveau du récepteur. Concernant la problématique de la mobilité, nous avons retenu et analysé un scénario prenant en considération les différentes situations rencontrées dans un modèle réel. Un algorithme de résolution multi-couvertures est proposé afin de traiter l'accès dans les zones de recouvrement. Cette étude a mené à distinguer trois régimes de mobilité : faible, moyen et fort. Les performances sont évaluées en fonction des métriques MAC et pour chaque mode de mobilité, un schéma de synthèse est établi
28
Exposito, Garcia Ernesto José. "Spécification et mise en oeuvre d'un protocole de transport orienté Qualité de Service pour les applications multimédias." Toulouse, INPT, 2003. http://www.theses.fr/2003INPT028H.
Full textAbstract:
De nos jours, des applications multimédia présentant de fortes contraintes temporelles, de bande passante et de synchronisation multimédia ont été conçues. Ces applications sont aussi capables de tolérer un service de communication imparfait (c'est-à-dire un service partiellement ordonné et/ou partiellement fiable). Cependant, les services de communication actuellement disponibles au niveau transport ou réseaux ne satisfont pas entièrement ces besoins complexes de Qualité de Service (QdS). Cette thèse propose la conception d'un protocole de transport de nouvelle génération orienté QdS : QoSTP (Quality of Service oriented Transport Protocol). Ce protocole a été conçu afin de fournir un ensemble important de mécanismes de transport répondant précisément aux exigences applicatives, tout en utilisant les ressources et les services réseaux disponibles. En outre, QoSTP a été spécifié dans le cadre d'un contexte standard de QdS capable de fournir un espace sémantique extensible et une architecture composable. Ce principe de modélisation facilite l'extension et la spécialisation du protocole pour répondre à un grand nombre de besoins applicatifs tout en tenant compte de l'ensemble des services offerts par le système de communication. La conception de QoSTP a suivi une méthodologie spécialisée basée sur le procédé unifié de développement ou Unified Development Process et sur l'utilisation des langages UML et SDL. Cette méthodologie propose trois étapes de modélisation : la définition d'un modèle global, la définition technique du service transport et la spécification comportementale du protocole. Des scénarios spécifiques de simulation ont été établis afin de valider la spécification. Des expériences mettant en œuvre des applications multimédia standards ont permis d'évaluer les performances de ce protocole. Une étude proposant une méthodologie de déploiement basée sur des nœuds programmables dans le cadre d'architectures multimédia distribuées a aussi été réalisée.
29
Zouinkhi, Ahmed. "Contribution à la modélisation de produit actif communicant, Spécification et Evaluation d'un protocole de communication orienté sécurité des produits." Phd thesis, Université Henri Poincaré - Nancy I, 2011. http://tel.archives-ouvertes.fr/tel-00594402.
Full textAbstract:
La surveillance d'entrepôts de produits chimiques est une opération délicate dans le sens où elle passe par une connaissance de la nature de chaque produit stocké, sur leur localisation, sur leur possible interaction et sur les actions à mettre en œuvre en cas d'alerte. Pour faciliter cette gestion de stockage, cette thèse propose d'utiliser le concept de l'ambiant où le produit possède son propre système d'information et de communication sans fil de façon à le rendre intelligent et autonome. Cette thèse propose et développe un modèle de comportement interne de produit actif permettant une approche distribuée de sécurité active. Celui-ci permet d'aboutir à un protocole de communication de niveau applicatif à embarquer dans les produits actifs. Ce protocole est évalué de façon formelle en utilisant les Réseaux de Petri colorés hiérarchiques. Finalement, ce protocole est implémenté dans le simulateur Castalia/Omnet++ pour l'analyser dans plusieurs scénarii et aussi pour l'éprouver lors du passage à l'échelle. Les résultats montrent l'intérêt et la faisabilité du concept de produit actif.
30
Zouinkhi, Ahmed. "Contribution à la modélisation de produit actif communicant : spécification et évaluation d'un protocole de communication orienté sécurité des produits." Thesis, Nancy 1, 2011. http://www.theses.fr/2011NAN10010/document.
Full textAbstract:
La surveillance d'entrepôts de produits chimiques est une opération délicate dans le sens où elle passe par une connaissance de la nature de chaque produit stocké, sur leur localisation, sur leur possible interaction et sur les actions à mettre en oeuvre en cas d'alerte. Pour faciliter cette gestion de stockage, cette thèse propose d'utiliser le concept de l'ambiant où le produit possède son propre système d'information et de communication sans fil de façon à le rendre intelligent et autonome. Cette thèse propose et développe un modèle de comportement interne de produit actif permettant une approche distribuée de sécurité active. Celui-ci permet d'aboutir à un protocole de communication de niveau applicatif à embarquer dans les produits actifs. Ce protocole est évalué de façon formelle en utilisant les Réseaux de Petri colorés hiérarchiques. Finalement, ce protocole est implémenté dans le simulateur Castalia/Omnet++ pour l'analyser dans plusieurs scénarii et aussi pour l'éprouver lors du passage à l'échelle. Les résultats montrent l'intérêt et la faisabilité du concept de produit actifMonitoring of chemical product storage is a delicate operation in the sense that it requires knowledge of the nature of each stored product, their location, their interaction and possible actions to be implemented in case of emergency. To facilitate the storage management, this thesis proposes to use the concept of ambient where the product has its own information system and wireless communication so as to make it intelligent and autonomous. This thesis proposes and develops a model of internal behavior of active product that allows a distributed approach of active security. This can lead to a communication protocol of application level to embed the active products. This protocol is formally assessed using hierarchical colored Petri nets. Finally, this protocol is implemented in the simulator Castalia/Omnet++ to analyze it in several scenarios and also for the experience when going to scale. The results show the usefulness and feasibility of the concept of active product
31
Villemur, Thierry. "Conception de services et de protocoles pour la gestion de groupes coopératifs." Phd thesis, Université Paul Sabatier - Toulouse III, 1995. http://tel.archives-ouvertes.fr/tel-00146528.
Full textAbstract:
Le travail coopératif est un domaine qui étudie le travail de groupes d'utilisateurs de façon générale. Sa finalité est la conception de collecticiels, ensembles logiciels qui contiennent les outils, les applications, et les plate-formes qui supportent les activités de groupes d'utilisateurs. La gestion de ces groupes et les échanges d'information entre leurs membres nécessitent la définition de nouveaux services de communication adaptés aux besoins des agents en coopération. Les travaux menés dans ce mémoire ont consisté à définir, à concevoir et à gérer la structuration des groupes coopératifs. Un modèle à base de graphes a été proposé à partir du partage de données, pour représenter les relations entre les divers membres d'un groupe coopératif. A partir de ce modèle, un service pour l'entrée et la sortie en coopération des agents coopérants a été défini. Un protocole de communication sous-jacent a été spécifié en utilisant le langage de description formelle Estelle. Le protocole proposé a été vérifié en utilisant l'environnement à base de réseaux de Petri VAL, puis a été implanté en langage C sous UNIX à partir du code Estelle généré. Une extension de ce travail permet la formation d'apartés qui sont des sous-groupes très dynamiques créés à l'intérieur de la coopération. Un autre protocole spécifié en Estelle a été proposé pour gérer la formation de ces apartés et leur évolution au sein de la coopération. En plus de la structuration des groupes, une étude des données qui peuvent être échangées entre des agents coopérants a mené à la définition d'un service de gestion des dépendances de données. Ce service, spécifié également en Estelle, permet de créer, supprimer ou modifier des dépendances entre données, et répercute les modifications de valeurs vers l'ensemble des données dépendantes.
32
Diaz, Nava Mario. "Proposition d'une méthodologie de conception de circuits intégrés de communication : réalisation d'un communicateur pour le réseau local FIP." Phd thesis, Grenoble INPG, 1986. http://tel.archives-ouvertes.fr/tel-00320454.
Full textAbstract:
FIP=Factory Instrumentation Protocol. On réalise un circuit intégré de communication pour le réseau FIP, projet national de communication entre automates réflexes, capteurs et actionneurs. Le circuit intégré est spécifié pour permettre soit la connexion de capteurs simples, soit la connexion de capteurs intelligents ou des automates de réseau. La conception de ce circuit intégré «à la demande» résulte d'une méthodologie originale. Cette méthodologie est orientée vers la conception de circuits VLSI de communication à partir d'une bibliothèque d'opérateurs flexibles, d'une part pour réduire le temps de conception, d'autre part pour donner la possibilité aux ingénieurs non spécialistes en conception de concevoir eux-mêmes leur circuit
33
Matiedje, Tawa Jeanne. "Extension événementielle d'une méthode formelle légère et application à l'analyse du protocole distribué Chord." Thesis, Toulouse, ISAE, 2019. http://www.theses.fr/2019ESAE0029.
Full textAbstract:
Cette étude concerne l’utilisation de la logique du premier ordre et la logique temporelle linéaire pour la spécification et la vérification des systèmes dynamiques ayant des structures riches. Elle concerne l’étude de la correction de fonctionnement du protocole de recherche distribuée Chord. L’objectif est d’une part d’améliorer la spécification et la vérification des systèmes dans le langage formel Electrum qui est une extension dynamique du langage formel Alloy basé sur la logique du premier ordre temporelle linéaire.Pour ce faire, nous avons développé une couche syntaxique au-dessus d’Electrum. L’objectif de cette couche est de faciliter la spécification du comportement dans Electrum, pour ce faire, nous avons défini une syntaxe permettant de générer automatiquement une partie de la spécification du comportement. Par ailleurs cette couche permet également de réduire les erreurs de spécification en déchargeant les utilisateurs de la spécification de certaines tâches comportementales ardues et sujettes aux erreurs.D’autre part, l’objectif est d’analyser formellement la correction de la propriété fondamentale de vivacité du protocole Chord. Pour ce faire nous avons spécifié et vérifié le protocole Chord avec l’extension d’Electrum que nous avons développée, puis nous avons prouvé sa correction et montré les avantages de notre méthode d’analyseThis study deals with the use of first-order logic and linear temporal logic for specificationand verification of dynamics system with rich structural properties. It also concerns the studyof the operating safety of the distributed lookup protocol Chord. The aim is on the one hand toimprove the specification and verification of systems whith the formal language Electrum a dynamicextension of the formal language Alloy based on first-order linear temporal logic. To do this, we havedeveloped an action layer above Electrum. The purpose of this layer is to make the specification ofthe behavior in Electrum easier, to do this, we have defined a syntax to automatically generate partof the specification of the behavior. Moreover, this layer also makes it possible to reduce specificationerrors by getting rid the users of the specification of certain laborious and error-prone behavioraltasks. On the other hand, the aim is the formal analyzing of the fundamental liveness property ofthe Chord protocol. To do this, we specified and verified the Chord protocol with the extension ofElectrum that we have developed, then we proved its correctness and showed the advantages of ouranalysis method
34
Gineste, Mathieu. "Spécification d'un cadre générique pour l'expression et le déploiement de la Qualité de Service dans les architectures de communication : application à une architecture de communication par satellite." Paris 6, 2006. http://www.theses.fr/2006PA066267.
Full textAbstract:
L’évolution des applications vers le multimédia et des réseaux vers une hétérogénéité d’architectures protocolaires, a placé la notion de Qualité de Service au cœur des architectures de communication émergentes ; Ceci soulève la question de l’expression de la QdS et de l’adaptation aux besoins applicatifs de la diversité des services disponibles. Cette thèse propose un cadre sémantique et syntaxique pour décrire les contraintes applicatives et les services sous-jacents, et sélectionner et composer les services de communication, répondant aux besoins applicatifs. Les systèmes satellitaires intègrent une propriété naturelle de diffusion de l’information, ce qui en fait un composant de l’Internet de nouvelle génération. Nous montrons comment, grâce au cadre générique, les services orientés gestion de QdS spécifiques d’une architecture de communication satellitaire peuvent être composés, afin de délivrer une adaptation efficace entre les ressources satellitaires et les besoins applicatifs.
35
Romero-Hernandez, Ivan. "Modélisation, spécification formelle et vérification de protocoles d'interaction: une approche basée sur les rôles." Phd thesis, 2004. http://tel.archives-ouvertes.fr/tel-00266421.
Full textAbstract:
Dans cette thèse on présente une proposition pour la spécification de protocoles de communication utilisés dans le contexte de systèmes multiagent, et qui nous appelons basée sur rôles. L'idée de rôle est récurrente dans le domaine de systèmes multiagent, et représente ce qui fait un agent dans une organisation, c'est à dire, la fonctionnalité qui est accomplie par l'agent dans le système, fonctionnalité qui est exprimée très souvent sous la forme d'échanges de messages qui suivent un protocole o séquence predéfinie. En nous centrant exclusivement sur l'aspect de l'interaction, il est possible d'abstraire la fonctionnalité du système en termes de séquences de messages stéréotypées. Séquences qui peuvent être utilisées comme un méthode de spécification en choisissant une notation appropriée. Nous proposons ici un processus de traduction à partir d'une notation visuelle inspirée de la proposition AUML, qui peut représenter le processus de communication dans un système multiagent, et le traduire vers une représentation formelle en Promela pour effectuer sa validation.
36
Zemmouri, Fathya. "Un modèle de validation automatique de mécanismes de sécurisation des communications." Thèse, 2003. http://hdl.handle.net/1866/14537.
Full text