Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.
Concept
Vérification de modèles
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.
Source officielle
À 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.