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

Calendrier et analyse des performances : vérification du modèle

Description

Cette séance de cours de l'instructeur de l'Université d'Aalborg au Danemark porte sur l'analyse du moment et des performances à l'aide de la vérification des modèles, y compris les tâches telles que l'analyse WCET et l'analyse de l'échéancier. Il traite également des résultats expérimentaux, de l'établissement de calendriers objectifs multiples et d'un suivi des cas sur le système TERMA.

Source officielle

Concepts associés (32)

Vérification de modèles

thumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.

Théorie des automates

En informatique théorique, l'objectif de la théorie des automates est de proposer des modèles de mécanismes mathématiques qui formalisent les méthodes de calcul.

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).

Rate-monotonic scheduling

L'ordonnancement à taux monotone (en anglais, rate-monotonic scheduling) est un algorithme d'ordonnancement temps réel en ligne à priorité constante (statique). Il attribue la priorité la plus forte à la tâche qui possède la plus petite période. RMS est optimal dans le cadre d'un système de tâches périodiques, synchrones, indépendantes et à échéance sur requête avec un ordonnanceur préemptif. De ce fait, il n'est généralement utilisé que pour ordonnancer des tâches vérifiant ces propriétés.

Optimum de Pareto

Un optimum de Pareto est une allocation des ressources sans alternative, c'est-à-dire que tous les agents économiques sont dans une situation telle qu'il est impossible d'améliorer le sort de l'un d'entre eux sans réduire la satisfaction d'un autre. Concept majeur de la microéconomie, il porte le nom de l'économiste italien Vilfredo Pareto, qui l'a utilisé pour décrire un état de la société dans lequel on ne peut pas améliorer le bien-être d’un individu sans détériorer celui d’un autre.

Afficher plus

Séances de cours associées (31)

Systèmes hybrides stochastiques

Explore la vérification des modèles de détermination du temps, la planification U-Pool, l'analyse des pires temps d'exécution et la vérification statistique des modèles pour les systèmes cyber-physiques.

MicroC/OS-II: Aperçu du noyau en temps réel

Fournit un aperçu de MicroC/OS-II, un noyau en temps réel avec des capacités multitâches et des fonctions déterministes, couvrant des sujets tels que la gestion des tâches, le noyau et la communication intertâche.

Tests automatisés : Fuzzing et sanitisation

Explore le flou, les oracles de bogues, les revues de codes et les techniques de test automatisé, soulignant l'importance de la désinfection pour détecter les défauts.

Raisonnement automatisé : vérification formelle avec LISA

Examine la vérification formelle à l'aide de l'assistant d'épreuve LISA et du vérificateur d'équivalence OCBSL.

Systèmes critiques de sécurité efficaces

Plonge dans la construction de systèmes efficaces et critiques pour la sécurité, en soulignant l'importance des pires délais d'exécution et les défis de l'intégration des considérations d'efficacité dans les processus de conception.

Afficher plus

Concepts associés (32)

Vérification de modèles

Théorie des automates

En informatique théorique, l'objectif de la théorie des automates est de proposer des modèles de mécanismes mathématiques qui formalisent les méthodes de calcul.

Méthode formelle (informatique)

Rate-monotonic scheduling

Optimum de Pareto

Afficher plus