• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 98
  • 24
  • 15
  • Tagged with
  • 138
  • 138
  • 49
  • 44
  • 43
  • 42
  • 42
  • 41
  • 36
  • 26
  • 21
  • 21
  • 20
  • 20
  • 19
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Méthodes et outils d'aide à la conception des processus opérationnels d'un système de formation / Methods and tools for assisting the design of operational precesses in education systems

Bistorin, Olivier 12 December 2007 (has links)
L'accession a l'éducation d'un nombre toujours plus grand d'individus a conduit a considérer la performance des systèmes de formation comme un véritable facteur de développement économique. C'est dans ce contexte que s'inscrivent nos travaux de thèse qui ont visé au développement de méthodes et outils pour l'aide à la conception de la partie opérationnelle d'un système de formation et notamment tout le système de transformation permettant l'accroissements de compétences chez les apprenants. Après avoir présenté un bilan des systèmes de formation en définissant leur périmètre puis leur fonctionnement et résultats, nous précisons alors les facteurs qui nous ont conduits a nous préoccuper des processus opérationnels des systèmes de formation. Dans un deuxième chapitre, nous précisons la démarche que nous avons choisi d'adopter et déclinons ainsi l'ensemble de notre méthode, associée a des outils spécifiques, qui vise à l'aide a la conception et la mise en oeuvre des formations. Nous nous éloignons de la logique de l'offre pour migrer vers une logique de la demande. Nous proposons une identification contraintes subies par un système de formation (ressources à capacité finie, cohérence pédagogique, indisponibilité de ressources, compétences et aptitudes des ressources, etc.) - - Dans une troisième partie, nous illustrons notre propos en appliquant les méthodes et outils développes a un cas pratique. Enfin, nous concluons sur l'apport scientifique constitué par ces travaux et ouvrons la voie vers de nombreuses perspectives, le domaine de l'ingénierie de la formation étant encore à ses balbutiements / The accession with the education of a number increasingly larger indivlduals resulted in regarding the performance of the systems of formation as a true factor of economic development. It is in ths context that our work of thesis is registered which aimed to the development of methods and tools for the assistance with the design of the operational part of an education system and in particular al the transformation s y s t v leading to the increase of students competences. After having presented an assessment of the education systems by defining their perimeter, their operation and results, we specify the factors whch led us to worry us about operational processes of the education systems. In a second chapter, we specifi the steps whch we chose to adopt and we decline the whole of our method, associated to specific tools, which aims to the assistance to the design and the setting of formations. We move away from the logic of supply to migrate towards logic of demand. We propose an identification of constraints in education systems (resources with limited capaciîy, teachmg coherence, unavailability of resources, competences and aptitudes of the resources, etc.) In a third part, we illustrate our concept by applying methods and tools developed with a practical case. Lastly, we conclude on the scientific contribution made up by t h work and open the way towards rnany prospects, the field of the engineering of the formation being still to its beginnings
2

Test and diagnosis of discrete event systems using Petri nets / Test et diagnostic des systèmes à événements discrets par les réseaux de Petri

Pocci, Marco 23 September 2013 (has links)
Le test d’identification d’état d’un système à événement discret (SED) a pour but d’en identifier l’état final, lorsque son état initial est inconnu. Une solution classique à ce problème, en supposant que le SED n’ait pas de sorties observables, consiste à déterminer une séquences de synchronisation, c.à-d., une séquence d’événements d’entrée qui conduit le SED sur un état connu. Ce problème a été résolu dans les années 60’ à l’aide des automates. L’objectif principal de cette thèse est d’utiliser les réseaux de Petri (RdP) pour obtenir une résolution plus optimal de ce problème et pour une plus large classe de systèmes.Initialement, nous montrons que la méthode classique peut être aisément étendue aux RdP synchronisés. Pour cette classe de réseaux non-autonomes, toute transition est associée à un événement d’entrée.L’approche proposée est générale, dans la mesure où elle s’applique à des RdP bornés arbitraires. Cependant, elle engendre le problème d’explosion combinatoire du nombre d’états. Pour obtenir des meilleures solutions, nous considérons une classe spéciale de RdP : les graphes d’état (GdE). Pour ces réseaux, nous considérons d’abord les GdE fortement connexes et proposons des approches pour la construction de SS, qui exploitent les propriétés structurelles du réseau en évitant ainsi une énumération exhaustive de l’espace d’état. Ces résultats s’étendent aux GdE non fortement connexes et à tout RdP synchronisé composé de GdE. Enfin, nous considérons la classe des RdP non bornés et proposons des séquences qui synchronisent le marquage des places non bornées. Une boîte à outils fournit toutes les approches décrites et est appliquée à des différents bancs d’essai. / State-identification experiments are designed to identify the final state of a discrete event system (DES) when its initial state is unknown. A classical solution, assuming the DES has no observable outputs, consists in determining a synchronizing sequence (SS), i.e., a sequence of input events that drives the system to a known state. This problem was essentially solved in the 60’ using automata. The main objective of this thesis is to use Petri nets (PNs) for solving the state-identification problem more efficiently and for a wider class of systems.We start showing that the classical SS construction method based on automata can be easily applied to synchronized PNs, a class of non-autonomous nets where each transition is associated with an input event. The proposed approach is fairly general and it works for arbitrary bounded nets with a complexity that is polynomial with the size of the state space. However, it incurs in the state-space explosion problem.Looking for more efficient solutions, we begin by considering a subclass of PNs called state machines (SMs). We first consider strongly connected SMs and propose a framework for SS construction that exploits structural criteria, not requiring an exhaustive enumeration of the state space of the net. Results are further extended to larger classes of nets, namely non strongly connected SMs and nets containing SM subnets. Finally we consider the class of unbounded nets that describe infinite state systems: even in this case we are able to compute sequences to synchronize the marking of bounded places. A Matlab toolbox implementing all approaches previously described has been designed and applied to a series of benchmarks.
3

Testing concurrent systems through event structures / Test de systèmes concurrents à l'aide de structures d'événements

Ponce de León, Hernan 07 November 2014 (has links)
Les systèmes logiciels complexes sont omniprésents dans notre vie quotidienne. De ce fait, un dysfonctionnement peut occasionner aussi bien une simple gêne qu'un danger mettant en péril des vies humaines. Le test est l'une des techniques les plus répandues (en particulier dans l'industrie) pour détecter les erreurs d'un système. Lorsque le cahier des charges d'un système est décrit par une spécification formelle, le test de conformité est utilisé pour garantir un certain niveau de confiance dans la correction d'une implémentation de ce système - dans ce cadre, la relation de conformité formalise la notion de correction. Cette thèse se focalise sur le test de conformité pour les systèmes concurrents. Le test de conformité pour les systèmes concurrents utilise principalement des modèles qui interprètent la concurrence par des entrelacements. Néanmoins, cette approche souffre du problème de l'explosion de l'espace d'états et elle n'offre pas la possibilité de tester certaines propriétés de la spécification telle que l'indépendance entre actions. Pour ces raisons, nous utilisons une sémantique d'ordres partiels pour la concurrence. De plus, nous proposons une nouvelle sémantique qui permet à certaines actions concurrentes d'être entrelacées et en force d'autres à être implémentées indépendamment. Nous proposons une généralisation de la relation de conformité ioco où les spécifications sont des réseaux de Petri et leur sémantique d'ordres partiels est donnée par leur dépliage. Cette relation de conformité permet de préserver l'indépendance, dans l'implémentation, des actions spécifiées comme concurrentes. Nous présentons un cadre de test complet pour cette relation. Nous définissons la notion de cas de test globaux gérant la concurrence, réduisant ainsi non seulement la taille des cas de test mais aussi celle de la suite de tests. Nous montrons comment les cas de test globaux peuvent être construits à partir du dépliage de la spécification en s'appuyant sur une traduction SAT, et nous réduisons le problème de la sélection de tests à la sélection d'un préfixe fini de ce dépliage : nous définissons différents critères de sélection à partir de la notion d'événement limite (cut-off event). Enfin, en supposant que chaque processus d'un système distribué possède une horloge locale, nous montrons que la conformité globale peut être testée dans une architecture de test distribuée en utilisant seulement des testeurs locaux ne communiquant pas entre eux. / Complex systems are everywhere and are part of our daily life. As a consequence, their failures can range from being inconvenient to being life-threatening. Testing is one of the most widely accepted techniques (especially in industry) to detect errors in a system. When the requirements of the system are described by a formal specification, conformance testing is used to guarantee a certain degree of confidence in the correctness of an implementation- in this setting a conformance relation formalizes the notion of correctness. This thesis focuses on conformance testing for concurrent systems. Conformance testing for concurrent system has mainly focused on models that interpret concurrency by interleavings. This approach does not only suf- fer from the state space explosion problem, but also lacks the ability to test properties of the specification such as independence between actions. For such reasons, we focus not only on partial order semantics for concurrency, but also propose a new semantics that allows to interleave some actions while forcing others to be implemented as independent. We propose a generalization of the ioco conformance relation, based on Petri nets specifications and their partial order semantics given by their unfoldings, preserving thus independence of actions from the specification. A complete testing framework for this conformance relation is presented. We introduce the notion of global test cases which handle concurrency, reducing not only the size of the test case, but also the number of tests in the test suite. We show how global test cases can be constructed from the unfolding of the specification based on a SAT encoding and we reduce the test selection problem to select a finite prefix of such unfolding: different testing criteria are defined based on the notion of cut-off events. Finally, we show that assuming each process of a distributed system has a local clock, global conformance can be tested in a distributed testing architecture using only local testers without any communication.
4

Contribution à la modélisation et à l'analyse de la chaîne logistique en utilisant des réseaux de Petri / Contribution to modeling and analysis of supply chain using Petri nets

Benmansour, Nesrine 21 November 2013 (has links)
La modélisation de la chaîne logistique "CL", proposée dans cette contribution, adopte une vision globale et tendancielle du fonctionnement de la chaîne. Vu la complexité et la grande diversité de la CL, la modélisation s'appuie sur une démarche modulaire et générique fondée sur le potentiel des Réseaux de Petri Continus à Vitesse variable (RdPCV) tout en introduisant des concepts issus de l approche systémique. Notre modèle permet d'intégrer à la fois l aspect physique, informationnel et décisionnel de la CL et s adapte à la grande diversité de sa configuration. De plus, il permet, à travers sa description continue du phénomène de transfert des flux de la CL, de pallier les problèmes d explosion combinatoire inhérents à la taille importante de la chaîne. Contrairement aux modèles de la CL existants, notre modèle offre une lisibilité en termes d'analyse des interactions entre les différents acteurs de la chaîne, et donne une vision globale plus claire de l état de cette chaîne facilitant ainsi son analyse, l évaluation de sa performance et le pilotage de ses différents flux. / The proposed model for supply chain in this contribution adopts a global and trend vision of supply chain functioning. Given the complexity and diversity of the supply chain, the modeling follows a modular and generic approach based on the potential of variable speed continuous Petri nets (VCPNs) and the concepts of the systemic approach. Our model allows to integrate both physical, informational and decision-making aspect of the supply chain and it adapts to the great diversity of its configuration. Moreover, through its continuous description of the flow transfer phenomena within the chain, it overcomes the problems of combinatorial explosion related to the large size of the chain. Unlike existing supply chain models, our model provides clarity in terms of interactions analysis between the different actors in the chain, and gives a clearer global vision of the state of this chain thus facilitating its analysis, evaluation of its performance and management of its various flows.
5

Modélisation des systèmes temps-réel répartis embarqués pour la génération automatique d'applications formellement vérifiées

Vergnaud, Thomas 12 1900 (has links) (PDF)
La construction d'une application répartie fait en général intervenir une couche logicielle particulière, appelée intergiciel, qui prend en charge la transmission des données entre les différents noeuds de l'application. La conception d'applications pour les systèmes embarqués temps-réel implique la prise en compte de certaines contraintes spécifiques à ce domaine, que ce soit en terme fiabilité ou de dimensions à la fois temporelles et spatiales. Ces contraintes doivent notamment être respectées par l'intergiciel. L'objet de ces travaux est la description des applications temps-réel réparties embarquées en vue de configurer automatiquement l'intergiciel adéquat. L'étude se focalise sur la définition d'un processus de conception permettant d'intégrer les phases de description, de vérification et de génération de l'application complète. Pour cela, nous nous reposons sur le langage de description d'architecture AADL. Nous l'exploitons comme passerelle entre la phase de description de l'architecture applicative, les formalismes de vérification, la génération du code exécutable et la configuration de l'exécutif réparti. Nous montrons comment spécifier un exécutif pour AADL afin de produire automatiquement le code applicatif et l'intergiciel pour une application répartie. Nous montrons également comment exploiter ces spécifications pour produire un réseau de Petri afin d'étudier l'intégrité des flux d'exécution dans l'architecture. Afin de valider notre processus de conception, nous avons conçu et développé Ocarina, un compilateur pour AADL qui utilise l'intergiciel schizophrène PolyORB comme exécutif.
6

Modélisation et analyse temporelle par réseaux de Petri et logique linéaire

Riviere, Nicolas 26 November 2003 (has links) (PDF)
L'objectif de cette thèse est de contribuer à l'élaboration de méthodes d'aide à la conception de systèmes coopératifs en prenant en compte les contraintes temporelles de manière quantitative. L'approche développée est fondée sur les réseaux de Petri, la logique linéaire et les graphes de contraintes temporelles. C'est une approche orientée « événements » et non orientée « états » comme c'est souvent le cas dans les approches fondées sur les réseaux de Petri. Elle est décomposée en deux étapes : une étape d'analyse « qualitative » et une étape d'analyse « quantitative ». La première consiste à obtenir les relations de causalité entre les événements appartenant à un scénario donné. L'équivalence entre un arbre de preuve en logique linéaire et le processus fini obtenu par dépliage d'un réseau de Petri à partir du même marquage initial montre que ces relations sont des relations de précédence. L'introduction de la notion de séquent caractéristique permet de mettre en Suvre une approche compositionnelle des processus à partir des règles du calcul des séquents. La deuxième étape consiste à passer du graphe décrivant les relations de précédence à un graphe de contraintes temporelles exprimant de façon linéaire l'ensemble des contraintes temporelles quantitatives que doivent vérifier les dates des franchissements des transitions dans un scénario. Il devient ainsi possible d'exploiter tous les résultats des techniques classiques d'analyse et de propagation de contraintes. Cette démarche est complètement cohérente avec les réseaux de Petri p-temporels mais difficilement compatible avec les t-temporels car ils engendrent des ensembles de contraintes qui sont plus complexes. Nous avons illustré cette démarche par un problème simple d'ordonnancement de documents multimédias. Nous avons par la suite montré comment, pour les réseaux de Petri t-temporels, nous pouvions calculer les dates de franchissements et les durées de séjour des jetons dans les places en restant sous une fo rme symbolique dans le cadre de la sémantique faible.
7

Intelligence Ambiante Pro-Active : de la Spécification à l'Implémentation

Reignier, Patrick 16 September 2010 (has links) (PDF)
L'objectif de l'informatique ubiquitaire ou ambiante, telle que définit par Weiser dans son article de référence, est de faire disparaître l'informatique traditionnelle au profit d'un espace informatisé. L'ordinateur ambiant doit également offrir des capacités d'interaction plus naturelles, être transparent et utilisable sans effort. L'intelligence ambiante est la rencontre de l'intelligence artificielle et de l'informatique ambiante. Il s'agit de déterminer, grâce à l'ensemble des dispositifs de perception présents, l'activité des utilisateurs (le contexte) afin de mieux comprendre et anticiper leurs besoins et leur proposer automatiquement des services appropriés (assistants virtuels). On parle d'applications sensibles au contexte. La conception et la réalisation d'une application sensible au contexte est une tâche complexe, aussi bien du point de vue du développeur que de l'utilisateur final. Il est important de proposer une approche adaptée à ces deux catégories d'acteurs. Nous avons tout d'abord proposé un modèle formel de spécification de contexte permettant d'établir le dialogue entre l'utilisateur et le développeur de l'application. Notre objectif est ensuite de proposer des approches permettant d'automatiser une partie de la production du code de manière à raccourcir le chemin entre cette spécification du modèle de contexte et sa mise en oeuvre au sein d'une application. Dans le cadre de l'aide au développeur, nous avons proposé une approche basée sur l'apprentissage supervisé pour l'interprétation des données capteurs sous forme d'entités et de rôles. Cette interprétation des données capteurs sert d'entrée à la reconnaissance de contexte (scénarios). En nous appuyant sur une approche de type Ingénierie Dirigée par les Modèles, nous avons projeté la spécification du contexte vers deux méta-modèles pour la reconnaissance de scénarios : les réseaux de Petri synchronisés, et les réseaux de Petri Flous. Nous nous sommes également intéressés à l'apprentissage automatique d'un modèle de situations basé sur un ensemble d'observations annotées. Dans le cadre de l'aide à l'utilisateur final, nous avons proposé deux approches permettant à l'usager d'adapter précisément l'application à ses besoins réels. La première approche est basée sur une analyse hors ligne du comportement de l'application (apprentissage supervisé). La seconde approche propose une modification en situation (punition – récompense) en s'appuyant sur une approche de type apprentissage renforcé indirect.
8

Contribution à la modélisation et à la vérification de processus workflow

Sbaï, Zohra 13 November 2010 (has links) (PDF)
La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées.
9

Un cadre formel pour le développement orienté aspect : modélisation et vérification des interactions dues aux aspects

Mostefaoui, Farida January 2008 (has links)
Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal
10

Fiabilité et durabilité d'un système complexe dédié aux énergies renouvelables - Application à un système photovoltaïque

Laronde, Rémi 30 September 2011 (has links) (PDF)
Cette thèse traite l'étude de la fiabilité et de la durabilité des systèmes photovoltaïques (PV). Face à l'absence de retour d'expériences, réaliser une telle étude sous-entend, à la fois, de proposer des procédures expérimentales de qualification basées sur des essais accélérés conduits sur les composants critiques des systèmes PV, et de développer des outils de simulation de la fiabilité de l'assemblage de ces composants constituant un système considéré complexe. Ainsi dans un premier temps, nous nous sommes consacrés à l'étude de la fiabilité des modules PV. Une méthodologie originale basée sur les essais de dégradation accélérée nous a permis d'estimer la fiabilité de ces composants sous leurs deux modes prédominants de défaillance que sont la corrosion et la décoloration de l'encapsulant. L'originalité réside dans la prise en compte des variabilités des conditions environnementales et sur le couplage des essais accélérés et de dégradation. Un outil a été développé à cet effet. Dans un second temps, nous nous sommes placés à l'échelle des systèmes PV. Nous avons proposé de simuler certains paramètres caractérisant leur sûreté de fonctionnement en s'appuyant sur une représentation du système avec ces différents modes de fonctionnement et de dysfonctionnement (défaillances et dégradation) à l'aide de plusieurs Réseaux de Petri Stochastiques imbriqués sur plusieurs niveaux afin de se situer, pour chaque composant, aux échelles pour lesquelles les modes de défaillance pouvaient être saisis et formulés. Notre travail de thèse permet finalement de donner les bases méthodologiques et les outils de simulations pour qualifier et garantir la durée de vie de systèmes PV.

Page generated in 0.1045 seconds