Résumé
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. Sur le plan pratique, la vérification de modèles est devenue, au niveau industriel, la méthode de vérification de code et de systèmes matériels la plus populaire et la plus utilisée aujourd'hui. La vérification de modèles s'appuie sur la logique temporelle dont l'un des pionniers est Amir Pnueli, qui reçut le prix Turing en 1996 pour (). Le model checking commence avec les travaux d'Edmund M. Clarke, E. Allen Emerson, Jean-Pierre Queille et Joseph Sifakis au tout début des années 1980. Clarke, Emerson et Sifakis se sont vu attribuer le prix Turing 2007 pour leurs travaux sur le model checking. Dans cette section, on précise ce que l'on entend par modèle et propriété puis par le problème de model checking. thumb|378x378px|Système de transition d'états pour un distributeur de boissons. Le système est modélisé par un système de transition d'états. Il s'agit d'un graphe orienté : un sommet représente un état du système et chaque arc représente une transition, c'est-à-dire une évolution possible du système d'un état donné vers un autre état. Chaque état du graphe orienté est étiqueté par l'ensemble des propositions atomiques vraies à ce point d'exécution (par exemple, i=2, le processeur 3 est en attente). Un tel graphe est aussi appelé une structure de Kripke. On donne ici l'exemple d'un distributeur de boissons qui peut être dans 4 états : attente d'une pièce de monnaie, sélection d'une boisson, distribution d'une bouteille d'eau minérale et distribution d'une bouteille de jus d'orange.
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Cours associés (2)
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
MATH-659: Topics in dispersive PDE
This course assumes familiarity with beginning graduate level real analysis, complex analysis and functional analysis, and also basic harmonic analysis, as well as fundamental concepts from differenti
Séances de cours associées (33)
Invariants dans le compteur lié: comprendre les invariants inductifs
Explore les invariants dans un système de compteur borné et l'importance des invariants inductifs dans la vérification des propriétés du système.
Méthode de tarification hédoniste : Logement et biens environnementaux
Couvre la méthode de tarification hédoniste pour l'évaluation des prix implicites des marchandises et introduit la méthode d'évaluation éventuelle pour l'estimation de la valeur des marchandises environnementales.
Catastrophes, succès et invariants inductifs
Explore les catastrophes logicielles, les vérifications réussies, les systèmes de transition et les invariants dans les systèmes.
Afficher plus
Publications associées (163)

Formal Autograding in a Classroom (Experience Report)

Viktor Kuncak, Mario Bucev, Dragana Milovancevic, Samuel Chassot

We report our experience in enhancing automated grading in a functional programming course using formal verification. In our approach, we deploy a verifier for Scala programs to check equivalences between student submissions and reference solutions. Conseq ...
2024

The Complexity of Satisfiability Checking for Symbolic Finite Automata

Rodrigo Raya

We study the satisfiability problem of symbolic finite automata and decompose it into the satisfiability problem of the theory of the input characters and the monadic second-order theory of the indices of accepted words. We use our decomposition to obtain ...
2023

Architecture and Abstraction

Pier Vittorio Aureli

In this theoretical study of abstraction in architecture—the first of its kind—Pier Vittorio Aureli argues for a reconsideration of abstraction, its meanings, and its sources. Although architects have typically interpreted abstraction in formal terms—the p ...
The MIT Press2023
Afficher plus
Concepts associés (18)
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.
Logique temporelle linéaire
En logique, la logique temporelle linéaire (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin.
Réseau de Petri
Animated_Petri_net_commons.gif Un réseau de Petri (aussi connu comme un réseau de Place/Transition ou réseau de P/T) est un modèle mathématique servant à représenter divers systèmes (informatiques, industriels...) travaillant sur des variables discrètes. Les réseaux de Petri sont apparus en 1962, dans la thèse de doctorat de Carl Adam Petri. Les réseaux de Petri sont des outils graphiques et mathématiques permettant de modéliser et de vérifier le comportement dynamique des systèmes à événements discrets comme les systèmes manufacturiers, les systèmes de télécommunications, les réseaux de transport.
Afficher plus
MOOCs associés (3)
Parallel programming
With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th
Parallel programming
With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th
Parallel programming
With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th