Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Recherche sur les systèmes dignes de confiance

Description

Cette séance de cours donne un aperçu du programme de recherche sur les systèmes fiables, en soulignant la nécessité d'une fiabilité éprouvée dans les systèmes informatiques en raison de vulnérabilités croissantes dans les systèmes embarqués. L'instructeur discute des défis liés à la vérification de systèmes complexes, des concepts d'isolement physique et logique, des décisions de conception derrière le micronoyau SEL4 et de l'approche rigoureuse pour atteindre une véritable fiabilité dans les systèmes critiques.

Source officielle

Concepts associés (31)

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Gestion de la mémoire

La gestion de la mémoire est une forme de gestion des ressources appliquée à la mémoire de l'ordinateur. L'exigence essentielle de la gestion de la mémoire est de fournir des moyens d'allouer dynamiquement des portions de mémoire aux programmes à leur demande, et de les libérer pour réutilisation lorsqu'elles ne sont plus nécessaires. Ceci est essentiel pour tout système informatique avancé où plus d'un processus peuvent être en cours à tout moment. Catégorie:Architecture informatique Catégorie:Pages avec

Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet).

Unité de gestion de mémoire

Une unité de gestion mémoire (MMU pour memory management unit), parfois appelée unité de gestion de mémoire paginée (PMMU pour paged memory management unit), est un composant permettant de contrôler les accès qu'un processeur fait à la mémoire de l'ordinateur dans lequel il est placé. À l'époque des premiers microprocesseurs, il s'agissait d'un circuit intégré dédié. Puis le MMU a été intégré aux microprocesseurs, à partir du 80286 pour la gamme Intel x86, à partir du 68030 pour la gamme Motorola 680x0.

Complexité

La complexité caractérise le comportement d'un système dont les composants interagissent localement et de façon non linéaire, ce qui se traduit par un comportement difficilement prédictible. La complexité peut donc caractériser un système "composé d'un grand nombre d'éléments interagissant sans coordination centrale, sans plan établi par un architecte, et menant spontanément à l'émergence de structures complexes" (Alain Barrat, directeur de recherche au Centre de physique théorique de Marseille); mais aussi caractériser des systèmes composés de peu d'éléments (voir le chaos déterministe).

Afficher plus

Séances de cours associées (32)

Les poissons peuvent-ils voir l’eau? , Conception pour la durabilité

Explore les interventions de conception artisanale pour la durabilité dans différents domaines.

Transition vers des villes intelligentes : complexité et interdépendance MOOC: Villes intelligentes, gestion des infrastructures urbaines intelligentes

S'inscrit dans la complexité et les interdépendances de la transition vers des villes intelligentes, soulignant l'importance d'une approche holistique.

Étude de cas Ariane 501

Analyse l'étude de cas Ariane 501, en se concentrant sur les erreurs logicielles et les complexités du système qui ont conduit à un échec de lancement.

Systèmes linéaires: convergence et méthodes

Explore les systèmes linéaires, la convergence et les méthodes de résolution en mettant l'accent sur les besoins en temps et en mémoire du processeur.

Systèmes embarqués: Introduction

Couvre les bases des systèmes embarqués, le développement FPGA, les systèmes d'exploitation en temps réel et les différents types de systèmes d'exploitation.

Afficher plus

Concepts associés (31)

Vérification formelle

Gestion de la mémoire

Méthode formelle (informatique)

Unité de gestion de mémoire

Complexité

Afficher plus