• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 36
  • 18
  • 3
  • Tagged with
  • 57
  • 57
  • 57
  • 31
  • 28
  • 28
  • 24
  • 23
  • 15
  • 13
  • 13
  • 13
  • 12
  • 12
  • 10
  • 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

Robustness in timed automata : analysis, synthesis, implementation / Robustesse dans les automates temporisés : analyse, synthèse, implémentation

Sankur, Ocan 24 May 2013 (has links)
Les automates temporisés sont un formalisme qui permet de modéliser, vérifier, et synthétiser des systèmes temps-réels. Ils sont dotés d’une sémantique abstraite et mathé- matique, qui permet de formaliser et résoudre plusieurs problèmes de vérification et de synthèse. Cependant, les automates temporisés sont utilisés pour concevoir des modèles, plutôt que décrire des systèmes temps-réels entiers. Ainsi, une fois la phase de conception terminée, il reste à déterminer si les comportements du modèle correspondent à ceux d’un vrai système. Une étape importante de l’implémentation consiste à s’assurer de la robustesse du système. On considère une notion de robustesse sur les automates tem- porisés qui exige que les comportements soient préservés quand le modèle est sujet à des perturbations bornées. Dans cette thèse, plusieurs approches sont étudiées : Dans l’analyse de robustesse, on se demande si un automate temporisés donné préserve ses com- portements sous divers types de perturbations, et on cherche à calculer un majorant sur les perturbations tolérées. La synthèse robuste s’intéresse au calcul d’une loi de contrôle (ou une stratégie) qui guide le système, et tolère des perturbations d’une magnitude calculable. Enfin, dans l’implémentation robuste, on s’intéresse à transformer automatiquement un modèle donné pour le rendre robuste, tout en préservant ses comportements. Plusieurs modèles de perturbations sont considérés : erreurs de mesure de temps (élargissement de gardes), élimination des comportements limites (contraction de gardes), et la restriction du domaine du temps aux valeurs discrètes. On formalise également les problèmes de synthèse robuste comme des jeux entre le contrôleur et un environnement qui perturbe systèmatiquement tout délai choisi par une quantité bornée. Ces problèmes sont étudiés pour les automates temporisés, ainsi que leurs extensions- les jeux temporisés, et les automates et jeux temporisés pondérés. Plusieurs algorithmes d’analyse de robustesse parametrée contre l’élargissement de gardes et la contraction de gardes sont proposés. Deux variantes de la sémantique de jeu pour le problème de synthèse robuste sont également étudiées pour les automates temporisés et leurs extensions. Un logiciel d’analyse de robustesse contre la contraction de gardes, ainsi que des résultats expérimentaux sont présentés. Le problème de l’implémentation robuste est étudié dans deux contextes différents. Tous les algorithmes calculent également un majorant sur les perturbations que le modèle donné est capable de tolérer. / Timed automata are a formalism to model, verify, and synthesize real-time systems. They have the advantage of having an abstract mathematical semantics, which allow formalizing and solving several verification and synthesis problems. However, timed automata are intended to design models, rather than completely describe real systems. Therefore, once the design phase is over, it remains to check whether the behavior of an actual implementation corresponds to that of the timed automaton model. An important step before implementing a system design is ensuring its robustness. This thesis considers a notion of robustness that asks whether the behavior of a given timed automaton is preserved, or can be made so, when it is subject to small perturbations. Several approaches are considered: Robustness analysis seeks to decide whether a given timed automaton tolerates perturbations, and in that case to compute the (maximum) amount of tolerated perturbations. In robust synthesis, a given system needs to be controlled by a law (or strategy) which tolerates perturbations upto some computable amount. In robust implementation, one seeks to automatically transform a given timed automaton model so that it tolerates perturbations by construction. Several perturbation models are considered, ranging from introducing error in time measures (guard enlargement), forbidding behaviors that are too close to boundaries (guard shrinking), and restricting the time domain to a discrete sampling. We also formalize robust synthesis problems as games, where the control law plays against the environment which can systematically perturb the chosen moves, by some bounded amount. These problems are studied on timed automata and their variants, namely, timed games, and weighted timed automata and games. Algorithms for the parameterized robustness analysis against guard enlargements, and guard shrinkings are presented. The robust synthesis problem is studied for two variants of the game semantics, for timed automata, games, and their weighted extensions. A software tool for robustness analysis against guard shrinkings is presented, and experimental results are discussed. The robust implementation problem is also studied in two different settings. In all algorithms, an upper bound on perturbations that the given timed automaton tolerates can be computed.
2

Research on virtualisation technlogy for real-time reconfigurable systems / Étude des techniques de virtualisation pour des systèmes temps-réel et reconfigurables dynamiquement

Xia, Tian 05 July 2016 (has links)
Cette thèse porte sur l'élaboration d'un micro-noyau original de type hyperviseur, appelé Ker-ONE, permettant de gérer la virtualisation pour des systèmes embarqués sur des plateformes de type SoC et fournissant un environnement pour les machines virtuelles en temps réel. Nous avons simplifié l'architecture du micro-noyau en ne gardant que les caractéristiques essentielles requises pour la virtualisation, et fortement réduit la complexité de la conception du noyau. Sur cette base, nous avons mis en place un mécanisme capable de gérer des ressources reconfigurables dans un système supportant des machines virtuelles. Les accélérateurs matériels reconfigurables sont mappés en tant que dispositifs classiques dans chaque machine. Grâce à une gestion efficace de la mémoire dédiée, nous détectons automatiquement le besoins de ressources et permettons une allocation dynamique des ressources sur FPGA. Suite à diverses expériences et évaluations sur la plateforme Zynq-7000, combinant ARM et ressources FPGA, nous avons montré que Ker-ONE ne dégrade que très peu les performances en termes de temps d'exécution. Les surcoûts engendrés peuvent généralement être ignorés dans les applications réelles. Nous avons également étudié l'ordonnançabilité temps réel dans les machines virtuelles. Les résultats montrent que le respect de l'échéance des tâches temps réel est garanti. Nous avons également démontré que le noyau proposé est capable d'allouer des accélérateurs matériels très rapidement. / This thesis describes an original micro-kernel that manages virtualization and that provides an environment for real-time virtual machines. We have simplified the micro-kernel architecture by only keeping critical features required for virtualization, and massively reduced the kernel design complexity. Based on this micro-kernel, we have introduced a framework capable of DPR resource management in a virtual machine system. DPR accelerators are mapped as ordinary devices in each VM. Through dedicated memory management, our framework automatically detects the request for DPR resources and allocates them dynamically. According to various experiments and evaluations on the Zynq-7000 platform we have shown that Ker-ONE causes very low virtualization overheads, which can generally be ignored in real applications. We have also studied the real-time schedulability in virtual machines. The results show that RTOS tasks are guaranteed to be scheduled while meeting their intra-VM timing constraints. We have also demonstrated that the proposed framework is capable of virtual machine DPR allocation with low overhead.
3

Distribution d'une architecture modulaire intégrée dans un contexte hélicoptère

Bérard-Deroche, Émilie 12 December 2017 (has links) (PDF)
Les architectures modulaires intégrées (IMA) sont une évolution majeure de l'architecture des systèmes avioniques. Elles permettent à plusieurs systèmes de se partager des ressources matérielles sans interférer dans leur fonctionnement grâce à un partitionnement spatial (zones mémoires prédéfinies) et temporel (ordonnancement statique) dans les processeurs ainsi qu'une réservation des ressources sur les réseaux empruntés. Ces allocations statiques permettent de vérifier le déterminisme général des différents systèmes: chaque système doit respecter des exigences de bout-en-bout dans une architecture asynchrone. Une étude pire cas permet d'évaluer les situations amenant aux limites du système et de vérifier que les exigences de bouten- bout sont satisfaites dans tous les cas. Les architectures IMA utilisés dans les avions centralisent physiquement des modules de calcul puissants dans des baies avioniques. Dans le cadre d'une étude de cas hélicoptère, ces baies ne sont pas envisageables pour des raisons d'encombrement: des processeurs moins puissants, utilisés à plus de 80%, composent ces architectures. Pour ajouter de nouvelles fonctionnalités ainsi que de nouveaux équipements, le souhait est de distribuer la puissance de traitement sur un plus grand nombre de processeurs dans le cadre d'une architecture globale asynchrone. Deux problématiques fortes ont été mises en avant tout au long de cette thèse. La première est la répartition des fonctions avioniques associée à une contrainte d'ordonnancement hors-ligne sur les différents processeurs. La deuxième est la satisfaction des exigences de communication de bout-en-bout, dépendantes de l'allocation et l'ordonnancement des fonctions ainsi que des latences de communication sur les réseaux. La contribution majeure de cette thèse est la recherche d'un compromis entre la distribution des architectures IMA sur un plus grand nombre de processeurs et la satisfaction des exigences de communication de bout-en-bout. Nous répondons à cet enjeu de la manière suivante: - Nous formalisons dans un premier temps un modèle de partitions communicantes tenant en compte des contraintes d'allocation et d'ordonnancement des partitions d'une part et des contraintes de communication de bout-en-bout entre partitions d'autre part. - Nous présentons dans un deuxième temps une recherche exhaustive des architectures valides. Nous proposons l'allocation successive des fonctions avioniques en considérant au même niveau la problématique d'ordonnancement et la satisfaction des exigences de bout-en-bout avec des latences de communication figées. Cette méthode itérative permet de construire des allocations de partitions partiellement valides. La construction des ordonnancements dans chacun des processeurs est cependant une démarche coûteuse dans le cadre d'une recherche exhaustive. - Nous avons conçu dans un troisième temps une heuristique gloutonne pour réduire l'espace de recherche associé aux ordonnancements. Elle permet de répondre aux enjeux de distribution d'une architecture IMA dans un contexte hélicoptère. - Nous nous intéressons dans un quatrième temps à l'impact des latences de communication de bout-en-bout sur des architectures distribuées données. Nous proposons pour celles-ci les choix de réseaux basés sur les latences de communication admissibles entre les différentes fonctions avioniques. Les méthodes que nous proposons répondent au besoin industriel de l'étude de cas hélicoptère, ainsi qu'à celui de systèmes de plus grande taille.
4

Adaptability and reconfiguration of automotive embedded systems / Adaptabilité et reconfiguration des systémes embarqués automobiles

Belaggoun, Amel 10 October 2017 (has links)
Les véhicules modernes sont de plus en plus informatisés pour satisfaire les exigences de sureté les plus strictes et pour fournir de meilleures expériences de conduite. Par conséquent, le nombre d'unités de contrôle électronique (ECU) dans les véhicules modernes a augmenté de façon continue au cours des dernières années. En outre, les applications à calcul complexe offrent une demande de calcul plus élevée sur les ECU et ont des contraintes de temps-réel dures et souples, d'où le besoin d’une approche unifiée traitant les deux types de contraintes. Les architectures multi-cœur permettent d'intégrer plusieurs niveaux de criticité de sureté sur la même plate-forme. De telles applications ont été conçues à l'aide d'approches statiques; cependant, les approches dites statiques ne sont plus réalisables dans des environnements très dynamiques en raison de la complexité croissante et les contraintes de coûts strictes, d’où la nécessite des solutions plus souples. Cela signifie que, pour faire face aux environnements dynamiques, un système automobile doit être adaptatif; c'est-à-dire qu'il doit pouvoir adapter sa structure et / ou son comportement à l'exécution en réponse à des changements fréquents dans son environnement. Ces nouvelles exigences ne peuvent être confrontées aux approches actuelles des systèmes et logiciels automobiles. Ainsi, une nouvelle conception de l'architecture électrique / électronique (E / E) d'un véhicule doit être développé. Récemment, l'industrie automobile a convenu de changer la plate-forme AUTOSAR actuelle en "AUTOSAR Adaptive Platform". Cette plate-forme est développée par le consortium AUTOSAR en tant que couche supplémentaire de la plate-forme classique. Il s'agit d'une étude de faisabilité continue basée sur le système d'exploitation POSIX qui utilise une communication orientée service pour intégrer les applications dans le système à tout moment. L'idée principale de cette thèse est de développer de nouveaux concepts d'architecture basés sur l'adaptation pour répondre aux besoins d'une nouvelle architecture E / E pour les véhicules entièrement électriques (VEF) concernant la sureté, la fiabilité et la rentabilité, et les intégrer à AUTOSAR. Nous définissons l'architecture ASLA (Adaptive System Level in AUTOSAR), qui est un cadre qui fournit une solution adaptative pour AUTOSAR. ASLA intègre des fonctions de reconfiguration au niveau des tâches telles que l'addition, la suppression et la migration des tâches dans AUTOSAR. La principale différence entre ASLA et la plate-forme Adaptive AUTOSAR est que ASLA permet d'attribuer des fonctions à criticité mixtes sur le même ECU ainsi que des adaptations bornées temps-réel, tant dis que Adaptive AUTOSAR sépare les fonctions temps réel critiques (fonctionnant sur la plate-forme classique) des fonctions temps réel non critiques (fonctionnant sur la plate-forme adaptative). Pour évaluer la validité de notre architecture proposée, nous fournissons une implémentation prototype de notre architecture ASLA et nous évaluons sa performance à travers des expériences. / Modern vehicles have become increasingly computerized to satisfy the more strict safety requirements and to provide better driving experiences. Therefore, the number of electronic control units (ECUs) in modern vehicles has continuously increased in the last few decades. In addition, advanced applications put higher computational demand on ECUs and have both hard and soft timing constraints, hence a unified approach handling both constraints is required. Moreover, economic pressures and multi-core architectures are driving the integration of several levels of safety-criticality onto the same platform. Such applications have been traditionally designed using static approaches; however, static approaches are no longer feasible in highly dynamic environments due to increasing complexity and tight cost constraints, and more flexible solutions are required. This means that, to cope with dynamic environments, an automotive system must be adaptive; that is, it must be able to adapt its structure and/or behaviour at runtime in response to frequent changes in its environment. These new requirements cannot be faced by the current state-of-the-art approaches of automotive software systems. Instead, a new design of the overall Electric/Electronic (E/E) architecture of a vehicle needs to be developed. Recently, the automotive industry agreed upon changing the current AUTOSAR platform to the “AUTOSAR Adaptive Platform”. This platform is being developed by the AUTOSAR consortium as an additional product to the current AUTOSAR classic platform. This is an ongoing feasibility study based on the POSIX operating system and uses service-oriented communication to integrate applications into the system at any desired time. The main idea of this thesis is to develop novel architecture concepts based on adaptation to address the needs of a new E/E architecture for Fully Electric Vehicles (FEVs) regarding safety, reliability and cost-efficiency, and integrate these in AUTOSAR. We define the ASLA (Adaptive System Level in AUTOSAR) architecture, which is a framework that provides an adaptive solution for AUTOSAR. ASLA incorporates tasks-level reconfiguration features such as addition, deletion and migration of tasks in AUTOSAR. The main difference between ASLA and the Adaptive AUTOSAR platform is that ASLA enables the allocation of mixed critical functions on the same ECU as well as time-bound adaptations while adaptive AUTOSAR separates critical, hard real-time functions (running on the classic platform) from non-critical/soft-real-time functions (running on the adaptive platform). To assess the validity of our proposed architecture, we provide an early prototype implementation of ASLA and evaluate its performance through experiments.
5

Définition et réalisation d'un outil de vérification formelle de programmes LUSTRE

Ratel, Christophe 08 July 1992 (has links) (PDF)
Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes
6

Vérification de propriétés de programmes flots de données synchrones

Glory, Anne-Cecile 14 December 1989 (has links) (PDF)
Dans le cadre de cette thèse, nous nous intéressons à la vérification de systèmes réactifs critiques et temps réel développés a l'aide de langages flots de données synchrones. Plus particulièrement nous avons considéré les propriétés de sureté pour les applications réalisées dans un des deux langages, saga produit de Merlin Gerin/ses, ou lustre crée au LGI. La méthode de vérification, pour laquelle un prototype a été réalise, est l'évaluation de propriétés sur un modèle des programmes. Un langage de spécification adapte au contexte des systèmes réactifs temps réel, avec sa sémantique formelle, est défini; ce langage comprend plusieurs opérateurs temporels. Le désir d'automatiser la vérification a nécessité la définition de la sémantique formelle de saga. Plusieurs modèles pour les programmes ont alors été étudiés: les arbres des exécutions comme base d'expression commune des sémantiques, les graphes d'états et automates de contrôle pour la mise en œuvre de la vérification. L'utilisation de moyens existants de vérification, fondée sur l'évaluation de propriétés sur un modèle des programmes, a été étudiée et évaluée. Ces moyens sont relatifs a des logiques temporelles arborescentes et des mu-calculs propositionnels. Une nouvelle approche pour la spécification et la vérification de propriétés de sureté, mettant en œuvre les caractéristiques du langage lustre, est développée. Elle s'appuie sur l'utilisation de lustre lui-même comme langage de spécification et présente les avantages suivants: formalisme commun pour la programmation et la spécification, utilisation du compilateur pour la vérification, possibilité de preuves modulaires
7

Contrôle de qualité optimal d'applications multimédia

Strus, Loïc 19 September 2008 (has links) (PDF)
Ce manuscrit présente une méthode de contrôle de qualité de service à grain fin d'applications multimédia. Celle-ci permet le contrôle d'applications dont les actions sont paramétrées par des niveaux de qualité et dont les durées d'exécution ne sont pas connues. Le contrôle consiste en la construction d'un ordonnancement et le choix des niveaux de qualité respectant des propriétés de sûreté et d'optimalité. C'est-à-dire que l'on cherche à maximiser l'utilisation du budget de temps sans pour autant le dépasser tout en ayant un choix de qualité régulier. Le contrôleur utilise une politique de gestion de qualité permettant de choisir pour chaque action l'ordonnancement et le niveau de qualité respectant les contraintes de qualité de service. Nous étendons et améliorons les résultats précédents dans deux directions. La première propose une approche symbolique de la politique de gestion de qualité. Celle-ci utilise un diagramme de vitesses qui est une représentation graphique du comportement de l'application contrôlée. À partir de cette représentation, nous avons proposé une technique de contrôle permettant de relâcher le nombre d'appels au contrôleur tout en respectant les propriétés de sûreté et d'optimalité. Nous avons ensuite proposé une approche stochastique du problème basée sur des fonctions de distribution de probabilités pour les durées d'exécution des actions. Notre méthode donne la possibilité à l'utilisateur de fixer la criticité des contraintes temps-réel. Elle permet aussi de calculer à priori le taux attendu de dépassement des échéances. Ces résultats théoriques ont été appuyés par des expériences réalisées sur un encodeur vidéo s'exécutant sur machine nue.
8

Une infrastructure de simulation modulaire pour l'évaluation de performances de systèmes temps-réel

Decotigny, David 07 April 2003 (has links) (PDF)
Un système informatique est temps-réel lorsque ses traitements doivent vérifier des propriétés d'ordre à la fois logique et temporel. Dans ce travail, nous proposons un outil de simulation pour l'évaluation de tels systèmes. Il peut venir compléter les méthodes sûres d'analyse statique, en particulier lorsque le comportement temporel du système ou de son environnement est insuffisamment caractérisé. L'outil met l'accent sur la faculté de personnalisation du système simulé, la grande fidélité des comportements temporels reproduits grâce à une granularité de simulation ajustable, la possibilité de réutiliser du code d'application existant, et l'efficacité de simulation. Nous présentons aussi un modèle objet générique pour l'ordonnancement dynamique couvrant un grand nombre d'ordonnanceurs existants, et qui a été évalué grâce à l'outil. Nous détaillons enfin les moyens de prise en compte de la granularité de l'horloge système dans ces algorithmes, ainsi qu'une évaluation de leur impact.
9

Abstractions booléennes pour la vérification des systèmes temps-réel

Kang, Eunyoung 08 November 2007 (has links) (PDF)
Cette thèse présente un schéma formel et efficace pour la vérification de systèmes temps-réel. Ce schéma repose sur la combinaison par abstraction de techniques déductives et de model checking, et cette combinaison permet de contourner les limites de chacune de ces techniques. La méthode utilise le raffinement itératif abstrait (IAR) pour le calcul d'abstractions finies. Etant donné un système de transitions et un ensemble fini de prédicats, la méthode détermine une abstraction booléenne dont les états correspondent à des ensembles de prédicats. La correction de l'abstraction par rapport au système d'origine est garantie en établissant un ensemble de conditions de vérification, issues de la procédure IAR. Ces conditions sont à démontrer à l'aide d'un prouveur de théorèmes. Les propriétés de sûreté et de vivacité sont ensuite vérifiées par rapport au modèle abstrait. La procédure IAR termine lorsque toutes les conditions sont vérifiées. Dans le cas contraire, une analyse plus fine détermine si le modèle abstrait doit être affiné en considérant davantage de prédicats. Nous identifions une classe de diagrammes de prédicats appelés PDT (Predicate Diagram for Timed system) qui décrivent l'abstraction et qui peuvent être utilisés pour la vérification de systèmes temporisés et paramétrés.
10

Vers une prise en compte fine de la plate-forme cible dans la construction des systèmes temps réel embarqués critiques par ingénierie des modèles

Gilles, Olivier 29 April 2010 (has links) (PDF)
Une démarche classique d'ingénierie dirigée par les modèles (IDM) consiste à modéliser un problème, puis à générer le code source associé à partir de ce modèle. Cette approche, qui a été étendue succès aux systèmes temps-réel, réduit signicativement les erreurs. Le modèle développé suit généralement une approche fonctionnelle du problème ; celle-ci est cependant rarement optimale en terme de consommation de ressources. Pour les systèmes temps réel, cette limitation est acceptable : ce n'est plus le cas dans le contexte de systèmes temps-réels embarqués (TRE). Cette thèse propose d'associer l'approche IDM à un processus d'optimisation basé sur le modèle du système, pour pouvoir appliquer cette approche aux systèmes TRE. Pour cela, nous proposons d'utiliser ensemble trois solutions : d'une part, AADL, un langage de modélisation architecturale, qui permet de spécifier la composante non-fonctionnelle de l'application. Ensuite, REAL, un langage d'expression de contrainte, qui permet d'exprimer des contraintes sur le modèle. Finalement, un processus d'optimisation, qui permet de transformer un modèle naïf en modèle répondant aux performances requises, en se basant sur des heuristiques gloutonnes. Nous montrons comment cette approche permet d'automatiser le processus de développement, en limitant le rôle de l'architecte à la traduction des contraintes exprimées par le cahier des charges et à la conception d'un modèle naïf du problème.

Page generated in 0.0398 seconds